From 59cbbdb827a9e7f758e5e3604eeaec91b3af7a0d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= <supermanitu@gmail.com>
Date: Mon, 21 Oct 2024 10:51:39 +0100
Subject: [PATCH] Fix rrename_tvsubst for types with one variable kind

---
 Tools/mrbnf_tvsubst.ML | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Tools/mrbnf_tvsubst.ML b/Tools/mrbnf_tvsubst.ML
index 8dd112c..44f41fe 100644
--- a/Tools/mrbnf_tvsubst.ML
+++ b/Tools/mrbnf_tvsubst.ML
@@ -1538,7 +1538,7 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy =
             SELECT_GOALS (length As) (EVERY1 [
               K (Local_Defs.unfold0_tac ctxt (@{thm comp_def} :: maps (map snd o #IImsupps) some_defs)),
               REPEAT_DETERM o resolve_tac ctxt (
-                @{thms cmin1 cmin2 card_of_Card_order}
+                @{thms ordLeq_refl cmin1 cmin2 card_of_Card_order}
                 @ map (fn thm => @{thm ordLess_ordLeq_trans} OF [thm]) f'_prems
                 @ maps (fn mrbnf => [
                   MRBNF_Def.Un_bound_of_mrbnf mrbnf, MRBNF_Def.UNION_bound_of_mrbnf mrbnf