# HG changeset patch
# User wenzelm
# Date 1635358033 -7200
# Node ID eceb93181ad9c303ce39e60e9151184e431cdfb7
# Parent  5d91897a8e5420fdd824b6b64cd2fde2d469e7bc
more antiquotations;

diff -r 5d91897a8e54 -r eceb93181ad9 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Oct 27 11:47:42 2021 +0100
+++ b/src/HOL/Tools/record.ML	Wed Oct 27 20:07:13 2021 +0200
@@ -107,17 +107,11 @@
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;
 
-fun mk_cons_tuple (left, right) =
-  let
-    val (leftT, rightT) = (fastype_of left, fastype_of right);
-    val prodT = HOLogic.mk_prodT (leftT, rightT);
-    val isomT = Type (\<^type_name>\<open>tuple_isomorphism\<close>, [prodT, leftT, rightT]);
-  in
-    Const (\<^const_name>\<open>Record.iso_tuple_cons\<close>, isomT --> leftT --> rightT --> prodT) $
-      Const (fst tuple_iso_tuple, isomT) $ left $ right
-  end;
-
-fun dest_cons_tuple (Const (\<^const_name>\<open>Record.iso_tuple_cons\<close>, _) $ Const _ $ t $ u) = (t, u)
+fun mk_cons_tuple (t, u) =
+  let val (A, B) = apply2 fastype_of (t, u)
+  in \<^Const>\<open>iso_tuple_cons \<^Type>\<open>prod A B\<close> A B for \<^Const>\<open>tuple_iso_tuple A B\<close> t u\<close> end;
+
+fun dest_cons_tuple \<^Const_>\<open>iso_tuple_cons _ _ _ for \<open>Const _\<close> t u\<close> = (t, u)
   | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
 
 fun add_iso_tuple_type overloaded (b, alphas) (leftT, rightT) thy =
@@ -149,7 +143,7 @@
         [((Binding.concealed (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
 
     val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
-    val cons = Const (\<^const_name>\<open>Record.iso_tuple_cons\<close>, isomT --> leftT --> rightT --> absT);
+    val cons = \<^Const>\<open>iso_tuple_cons absT leftT rightT\<close>;
 
     val thm_thy =
       cdef_thy
@@ -171,8 +165,7 @@
       val goal' = Envir.beta_eta_contract goal;
       val is =
         (case goal' of
-          Const (\<^const_name>\<open>Trueprop\<close>, _) $
-            (Const (\<^const_name>\<open>isomorphic_tuple\<close>, _) $ Const is) => is
+          \<^Const_>\<open>Trueprop for \<^Const>\<open>isomorphic_tuple _ _ _ for \<open>Const is\<close>\<close>\<close> => is
         | _ => err "unexpected goal format" goal');
       val isthm =
         (case Symtab.lookup isthms (#1 is) of
@@ -937,7 +930,7 @@
 
 fun mk_comp_id f =
   let val T = range_type (fastype_of f)
-  in HOLogic.mk_comp (Const (\<^const_name>\<open>Fun.id\<close>, T --> T), f) end;
+  in HOLogic.mk_comp (\<^Const>\<open>id T\<close>, f) end;
 
 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
   | get_upd_funs _ = [];
@@ -1272,7 +1265,7 @@
    {lhss = [\<^term>\<open>r = s\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of
-        Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) $ _ $ _ =>
+        \<^Const_>\<open>HOL.eq T for _ _\<close> =>
           (case rec_id ~1 T of
             "" => NONE
           | name =>
@@ -1325,7 +1318,7 @@
       let
         val thy = Proof_Context.theory_of ctxt;
         val t = Thm.term_of ct;
-        fun mkeq (lr, Teq, (sel, Tsel), x) i =
+        fun mkeq (lr, T, (sel, Tsel), x) i =
           if is_selector thy sel then
             let
               val x' =
@@ -1334,23 +1327,22 @@
                 else raise TERM ("", [x]);
               val sel' = Const (sel, Tsel) $ Bound 0;
               val (l, r) = if lr then (sel', x') else (x', sel');
-            in Const (\<^const_name>\<open>HOL.eq\<close>, Teq) $ l $ r end
+            in \<^Const>\<open>HOL.eq T for l r\<close> end
           else raise TERM ("", [Const (sel, Tsel)]);
 
-        fun dest_sel_eq (Const (\<^const_name>\<open>HOL.eq\<close>, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
-              (true, Teq, (sel, Tsel), X)
-          | dest_sel_eq (Const (\<^const_name>\<open>HOL.eq\<close>, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
-              (false, Teq, (sel, Tsel), X)
+        fun dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ (Const (sel, Tsel) $ Bound 0) $ X) =
+              (true, T, (sel, Tsel), X)
+          | dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ X $ (Const (sel, Tsel) $ Bound 0)) =
+              (false, T, (sel, Tsel), X)
           | dest_sel_eq _ = raise TERM ("", []);
       in
         (case t of
-          Const (\<^const_name>\<open>Ex\<close>, Tex) $ Abs (s, T, t) =>
+          \<^Const_>\<open>Ex T for \<open>Abs (s, _, t)\<close>\<close> =>
            (let
              val eq = mkeq (dest_sel_eq t) 0;
              val prop =
                Logic.list_all ([("r", T)],
-                 Logic.mk_equals
-                  (Const (\<^const_name>\<open>Ex\<close>, Tex) $ Abs (s, T, eq), \<^term>\<open>True\<close>));
+                 Logic.mk_equals (\<^Const>\<open>Ex T for \<open>Abs (s, T, eq)\<close>\<close>, \<^Const>\<open>True\<close>));
             in
               SOME (Goal.prove_sorry_global thy [] [] prop
                 (fn {context = ctxt', ...} =>
@@ -1713,16 +1705,11 @@
     val T = Type (tyco, map TFree vs);
     val test_function = Free ("f", termifyT T --> \<^typ>\<open>(bool \<times> term list) option\<close>);
     val params = Name.invent_names Name.context "x" Ts;
-    fun full_exhaustiveT T =
-      (termifyT T --> \<^typ>\<open>(bool \<times> Code_Evaluation.term list) option\<close>) -->
-        \<^typ>\<open>natural\<close> --> \<^typ>\<open>(bool \<times> Code_Evaluation.term list) option\<close>;
-    fun mk_full_exhaustive T =
-      Const (\<^const_name>\<open>Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive\<close>,
-        full_exhaustiveT T);
+    fun mk_full_exhaustive U = \<^Const>\<open>full_exhaustive_class.full_exhaustive U\<close>;
     val lhs = mk_full_exhaustive T $ test_function $ size;
     val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
-    val rhs = fold_rev (fn (v, T) => fn cont =>
-        mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
+    val rhs = fold_rev (fn (v, U) => fn cont =>
+        mk_full_exhaustive U $ (lambda (Free (v, termifyT U)) cont) $ size) params tc;
   in
     (lhs, rhs)
   end;
@@ -1756,10 +1743,7 @@
 fun add_code ext_tyco vs extT ext simps inject thy =
   if Config.get_global thy codegen then
     let
-      val eq =
-        HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (Const (\<^const_name>\<open>HOL.equal\<close>, extT --> extT --> HOLogic.boolT),
-           Const (\<^const_name>\<open>HOL.eq\<close>, extT --> extT --> HOLogic.boolT)));
+      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (\<^Const>\<open>HOL.equal extT\<close>, \<^Const>\<open>HOL.eq extT\<close>));
       fun tac ctxt eq_def =
         Class.intro_classes_tac ctxt []
         THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]