# HG changeset patch
# User wenzelm
# Date 1632859972 -7200
# Node ID 79f484b0e35ba656f9e6e536331ed58c9dfef86e
# Parent  79ac28db185cf9466512a31ffdd04cecbe7f945f
clarified antiquotations;

diff -r 79ac28db185c -r 79f484b0e35b src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 28 22:12:52 2021 +0200
@@ -2215,7 +2215,7 @@
       let
         fun mk_goal c cps gcorec n k disc =
           mk_Trueprop_eq (disc $ (gcorec $ c),
-            if n = 1 then \<^const>\<open>True\<close>
+            if n = 1 then \<^Const>\<open>True\<close>
             else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
 
         val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
diff -r 79ac28db185c -r 79f484b0e35b src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Tue Sep 28 22:12:52 2021 +0200
@@ -42,7 +42,7 @@
   let
     fun instantiate_with_lambda thm =
       let
-        val prop as \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, fT) $ _) $ _) =
+        val prop as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>HOL.eq _ for \<open>Var (_, fT) $ _\<close> _\<close>\<close>\<close> =
           Thm.prop_of thm;
         val T = range_type fT;
         val j = Term.maxidx_of_term prop + 1;
diff -r 79ac28db185c -r 79f484b0e35b src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Sep 28 22:12:52 2021 +0200
@@ -385,7 +385,7 @@
     val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
     val all_algLam_alg_pointfuls = map (mk_pointful ctxt) all_algLam_algs;
 
-    val \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = code_goal;
+    val \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for lhs rhs\<close>\<close> = code_goal;
     val (fun_t, args) = strip_comb lhs;
     val closed_rhs = fold_rev lambda args rhs;
 
@@ -447,7 +447,7 @@
 
     val fp_nesting_Ts = map T_of_bnf fp_nesting_bnfs;
 
-    fun is_nullary_disc_def (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _
+    fun is_nullary_disc_def (\<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _
           $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _))) = true
       | is_nullary_disc_def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _
           $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _)) = true
@@ -512,7 +512,7 @@
     val goal = mk_Trueprop_eq (fun_t, abs_curried_balanced arg_Ts algrho);
 
     fun const_of_transfer thm =
-      (case Thm.prop_of thm of \<^const>\<open>Trueprop\<close> $ (_ $ cst $ _) => cst);
+      (case Thm.prop_of thm of \<^Const>\<open>Trueprop\<close> $ (_ $ cst $ _) => cst);
 
     val eq_algrho =
       Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
@@ -590,7 +590,7 @@
 
 fun derive_cong_ctr_intros ctxt cong_ctor_intro =
   let
-    val \<^const>\<open>Pure.imp\<close> $ _ $ (\<^const>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _ $ (ctor $ _))) =
+    val \<^Const_>\<open>Pure.imp\<close> $ _ $ (\<^Const_>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _ $ (ctor $ _))) =
       Thm.prop_of cong_ctor_intro;
 
     val fpT as Type (fpT_name, fp_argTs) = range_type (fastype_of ctor);
@@ -615,19 +615,19 @@
 
 fun derive_cong_friend_intro ctxt cong_algrho_intro =
   let
-    val \<^const>\<open>Pure.imp\<close> $ _ $ (\<^const>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _
+    val \<^Const_>\<open>Pure.imp\<close> $ _ $ (\<^Const_>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _
         $ ((algrho as Const (algrho_name, _)) $ _))) =
       Thm.prop_of cong_algrho_intro;
 
     val fpT as Type (_, fp_argTs) = range_type (fastype_of algrho);
 
-    fun has_algrho (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) =
+    fun has_algrho (\<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) =
       fst (dest_Const (head_of (strip_abs_body rhs))) = algrho_name;
 
     val eq_algrho :: _ =
       maps (filter (has_algrho o Thm.prop_of) o #eq_algrhos o snd) (all_friend_extras_of ctxt);
 
-    val \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ friend0 $ _) = Thm.prop_of eq_algrho;
+    val \<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ friend0 $ _) = Thm.prop_of eq_algrho;
     val friend = mk_ctr fp_argTs friend0;
 
     val goal = mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong friend;
@@ -654,8 +654,8 @@
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val \<^const>\<open>Pure.imp\<close> $ (\<^const>\<open>Trueprop\<close> $ (_ $ Abs (_, _, _ $
-        Abs (_, _, \<^const>\<open>implies\<close> $ _ $ (_ $ (cong0 $ _) $ _ $ _))))) $ _ =
+    val \<^Const_>\<open>Pure.imp\<close> $ (\<^Const_>\<open>Trueprop\<close> $ (_ $ Abs (_, _, _ $
+        Abs (_, _, \<^Const_>\<open>implies\<close> $ _ $ (_ $ (cong0 $ _) $ _ $ _))))) $ _ =
       Thm.prop_of dtor_coinduct;
 
     val SOME {X as TVar ((X_s, _), _), fp_res = {dtor_ctors, ...}, pre_bnf,
@@ -820,7 +820,7 @@
             |> curry (op ~~) (map (fn disc => disc $ lhs) discs);
 
           fun mk_disc_iff_props props [] = props
-            | mk_disc_iff_props _ ((lhs, \<^const>\<open>HOL.True\<close>) :: _) = [lhs]
+            | mk_disc_iff_props _ ((lhs, \<^Const_>\<open>True\<close>) :: _) = [lhs]
             | mk_disc_iff_props props ((lhs, rhs) :: views) =
               mk_disc_iff_props ((HOLogic.mk_eq (lhs, rhs)) :: props) views;
         in
@@ -2242,7 +2242,7 @@
 
     val fun_T =
       (case code_goal of
-        \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) => fastype_of (head_of t)
+        \<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) => fastype_of (head_of t)
       | _ => ill_formed_equation_lhs_rhs lthy [code_goal]);
     val fun_t = Const (fun_name, fun_T);
 
diff -r 79ac28db185c -r 79f484b0e35b src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML	Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML	Tue Sep 28 22:12:52 2021 +0200
@@ -367,7 +367,7 @@
           ctrXs_Tss
           |> map_index (fn (i, Ts) =>
             Abs (Name.uu, mk_tupleT_balanced Ts,
-              if i + 1 = k then \<^const>\<open>HOL.True\<close> else \<^const>\<open>HOL.False\<close>))
+              if i + 1 = k then \<^Const>\<open>True\<close> else \<^Const>\<open>False\<close>))
           |> mk_case_sumN_balanced
           |> map_types substXYT
           |> (fn tm => Library.foldl1 HOLogic.mk_comp [tm, rep, snd_const YpreT])
diff -r 79ac28db185c -r 79f484b0e35b src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Sep 28 22:12:52 2021 +0200
@@ -189,22 +189,22 @@
 
 fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs);
 
-val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^const>\<open>True\<close>;
-val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^const>\<open>False\<close>;
+val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^Const>\<open>True\<close>;
+val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^Const>\<open>False\<close>;
 val mk_dnf = mk_disjs o map mk_conjs;
 
-val conjuncts_s = filter_out (curry (op aconv) \<^const>\<open>True\<close>) o HOLogic.conjuncts;
+val conjuncts_s = filter_out (curry (op aconv) \<^Const>\<open>True\<close>) o HOLogic.conjuncts;
 
-fun s_not \<^const>\<open>True\<close> = \<^const>\<open>False\<close>
-  | s_not \<^const>\<open>False\<close> = \<^const>\<open>True\<close>
-  | s_not (\<^const>\<open>Not\<close> $ t) = t
-  | s_not (\<^const>\<open>conj\<close> $ t $ u) = \<^const>\<open>disj\<close> $ s_not t $ s_not u
-  | s_not (\<^const>\<open>disj\<close> $ t $ u) = \<^const>\<open>conj\<close> $ s_not t $ s_not u
-  | s_not t = \<^const>\<open>Not\<close> $ t;
+fun s_not \<^Const_>\<open>True\<close> = \<^Const>\<open>False\<close>
+  | s_not \<^Const_>\<open>False\<close> = \<^Const>\<open>True\<close>
+  | s_not \<^Const_>\<open>Not for t\<close> = t
+  | s_not \<^Const_>\<open>conj for t u\<close> = \<^Const>\<open>disj for \<open>s_not t\<close> \<open>s_not u\<close>\<close>
+  | s_not \<^Const_>\<open>disj for t u\<close> = \<^Const>\<open>conj for \<open>s_not t\<close> \<open>s_not u\<close>\<close>
+  | s_not t = \<^Const>\<open>Not for t\<close>;
 
 val s_not_conj = conjuncts_s o s_not o mk_conjs;
 
-fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^const>\<open>False\<close>] else cs;
+fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^Const>\<open>False\<close>] else cs;
 fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs;
 
 fun propagate_units css =
@@ -215,17 +215,17 @@
       (map (propagate_unit_pos u) (uss @ css'))));
 
 fun s_conjs cs =
-  if member (op aconv) cs \<^const>\<open>False\<close> then \<^const>\<open>False\<close>
-  else mk_conjs (remove (op aconv) \<^const>\<open>True\<close> cs);
+  if member (op aconv) cs \<^Const>\<open>False\<close> then \<^Const>\<open>False\<close>
+  else mk_conjs (remove (op aconv) \<^Const>\<open>True\<close> cs);
 
 fun s_disjs ds =
-  if member (op aconv) ds \<^const>\<open>True\<close> then \<^const>\<open>True\<close>
-  else mk_disjs (remove (op aconv) \<^const>\<open>False\<close> ds);
+  if member (op aconv) ds \<^Const>\<open>True\<close> then \<^Const>\<open>True\<close>
+  else mk_disjs (remove (op aconv) \<^Const>\<open>False\<close> ds);
 
 fun s_dnf css0 =
   let val css = propagate_units css0 in
     if null css then
-      [\<^const>\<open>False\<close>]
+      [\<^Const>\<open>False\<close>]
     else if exists null css then
       []
     else
diff -r 79ac28db185c -r 79f484b0e35b src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Sep 28 22:12:52 2021 +0200
@@ -154,7 +154,7 @@
 
 fun inst_split_eq ctxt split =
   (case Thm.prop_of split of
-    \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>
+    \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Var (_, Type (_, [T, _])) $ _\<close> _\<close>\<close> =>
     let
       val s = Name.uu;
       val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
diff -r 79ac28db185c -r 79f484b0e35b src/HOL/Tools/BNF/bnf_lfp_countable.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Tue Sep 28 22:12:52 2021 +0200
@@ -70,13 +70,13 @@
 
 fun encode_sumN n k t =
   Balanced_Tree.access {init = t,
-      left = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inl (nat, nat)} $ t),
-      right = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inr (nat, nat)} $ t)}
+      left = fn t => \<^Const>\<open>sum_encode for \<^Const>\<open>Inl \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for t\<close>\<close>,
+      right = fn t => \<^Const>\<open>sum_encode for \<^Const>\<open>Inr \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for t\<close>\<close>}
     n k;
 
-fun encode_tuple [] = \<^term>\<open>0 :: nat\<close>
+fun encode_tuple [] = \<^Const>\<open>zero_class.zero \<^Type>\<open>nat\<close>\<close>
   | encode_tuple ts =
-    Balanced_Tree.make (fn (t, u) => \<^const>\<open>prod_encode\<close> $ (@{const Pair (nat, nat)} $ u $ t)) ts;
+    Balanced_Tree.make (fn (t, u) => \<^Const>\<open>prod_encode for \<^Const>\<open>Pair \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for u t\<close>\<close>) ts;
 
 fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
   let
@@ -181,7 +181,7 @@
       |> map (Thm.close_derivation \<^here>)
     end;
 
-fun get_countable_goal_type_name (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
+fun get_countable_goal_type_name (\<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
     $ Abs (_, Type (_, [Type (s, _), _]), Const (\<^const_name>\<open>inj_on\<close>, _) $ Bound 0
         $ Const (\<^const_name>\<open>top\<close>, _)))) = s
   | get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";