# HG changeset patch
# User traytel
# Date 1736945583 -3600
# Node ID cd2521e39783fd719be53f2468b9f46a54b48c00
# Parent  6026394145593789bff350d567194cbde41e93b6
introduce fewer constants in copy_bnf/lift_bnf (by Jan van Brügge)

diff -r 602639414559 -r cd2521e39783 src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Tue Jan 14 22:35:03 2025 +0000
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Wed Jan 15 13:53:03 2025 +0100
@@ -436,7 +436,7 @@
 
     (* get the bnf for RepT *)
     val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) =
-      bnf_of_typ true Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
+      bnf_of_typ true Hardly_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
         Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy);
 
     val set_bs =
@@ -670,7 +670,7 @@
               [card_order_bd_tac, cinfinite_bd_tac, regularCard_bd_tac] @ set_bds_tac @
               [le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac];
 
-            val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I
+            val (bnf_G, lthy) = bnf_def Hardly_Inline (user_policy Note_Some) true I
               tactics wit_tac NONE map_b rel_b pred_b set_bs
               (((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G), SOME pred_G)
               lthy;
@@ -852,7 +852,7 @@
       map dest_TFree alpha0s |> filter (fn T => exists (fn Ts => member op= Ts T) Ass);
 
     val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) =
-      bnf_of_typ true Dont_Inline (Binding.qualify true absT_name) flatten_tyargs
+      bnf_of_typ true Hardly_Inline (Binding.qualify true absT_name) flatten_tyargs
         [] Ds0 repT ((empty_comp_cache, empty_unfolds), lthy);
     val live = length alphas;
     val _ = (if live = 0 then error "No live variables" else ());
@@ -1889,7 +1889,7 @@
             | mk_wit_tacs [] ws ctxt = mk_wit_tacs set_F'_thmss ws ctxt
             | mk_wit_tacs _ _ _ = all_tac;
 
-          val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I
+          val (bnf_G, lthy) = bnf_def Hardly_Inline (user_policy Note_Some) true I
             tactics (mk_wit_tacs [] wit_thms) NONE map_b rel_b pred_b set_bs
             (((((((Binding.empty, absT), map_G), sets_G), bd_G), wits_G), SOME rel_G), NONE) lthy;