# HG changeset patch
# User wenzelm
# Date 1632932482 -7200
# Node ID 5399dfe9141c2a7a0cb09d22da28219dbb5c0002
# Parent  b9331caf92c3346d42802028c70aa155cdebca9b
clarified antiquotations;

diff -r b9331caf92c3 -r 5399dfe9141c src/HOL/ex/Rewrite_Examples.thy
--- a/src/HOL/ex/Rewrite_Examples.thy	Wed Sep 29 11:55:09 2021 +0200
+++ b/src/HOL/ex/Rewrite_Examples.thy	Wed Sep 29 18:21:22 2021 +0200
@@ -222,9 +222,9 @@
       val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
       (* Note that the pattern order is reversed *)
       val pat = [
-        Rewrite.For [(x, SOME \<^typ>\<open>nat\<close>)],
+        Rewrite.For [(x, SOME \<^Type>\<open>nat\<close>)],
         Rewrite.In,
-        Rewrite.Term (@{const plus(nat)} $ Free (x, \<^typ>\<open>nat\<close>) $ \<^term>\<open>1 :: nat\<close>, [])]
+        Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>nat\<close> for \<open>Free (x, \<^Type>\<open>nat\<close>)\<close> \<^term>\<open>1 :: nat\<close>\<close>, [])]
       val to = NONE
     in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
   \<close>)
@@ -240,10 +240,10 @@
       val pat = [
         Rewrite.Concl,
         Rewrite.In,
-        Rewrite.Term (Free ("Q", (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) --> \<^typ>\<open>bool\<close>)
-          $ Abs ("x", \<^typ>\<open>int\<close>, Rewrite.mk_hole 1 (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^typ>\<open>int\<close>)]),
+        Rewrite.Term (Free ("Q", (\<^Type>\<open>int\<close> --> TVar (("'b",0), [])) --> \<^Type>\<open>bool\<close>)
+          $ Abs ("x", \<^Type>\<open>int\<close>, Rewrite.mk_hole 1 (\<^Type>\<open>int\<close> --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^Type>\<open>int\<close>)]),
         Rewrite.In,
-        Rewrite.Term (@{const plus(int)} $ Free (x, \<^typ>\<open>int\<close>) $ Var (("c", 0), \<^typ>\<open>int\<close>), [])
+        Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>Free (x, \<^Type>\<open>int\<close>)\<close> \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close>\<close>, [])
         ]
       val to = NONE
     in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
@@ -261,7 +261,7 @@
     Rewrite.Term (Free ("Q", (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) --> \<^typ>\<open>bool\<close>)
       $ Abs ("x", \<^typ>\<open>int\<close>, Rewrite.mk_hole 1 (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^typ>\<open>int\<close>)]),
     Rewrite.In,
-    Rewrite.Term (@{const plus(int)} $ Free (x, \<^typ>\<open>int\<close>) $ Var (("c", 0), \<^typ>\<open>int\<close>), [])
+    Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>Free (x, \<^Type>\<open>int\<close>)\<close> \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close>\<close>, [])
     ]
   val to = NONE
   val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct
@@ -274,7 +274,7 @@
   val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
   val pat = [
     Rewrite.In,
-    Rewrite.Term (@{const plus(int)} $ Var (("c", 0), \<^typ>\<open>int\<close>) $ Var (("c", 0), \<^typ>\<open>int\<close>), [])
+    Rewrite.Term (\<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close> \<open>Var (("c", 0), \<^Type>\<open>int\<close>)\<close>\<close>, [])
     ]
   val to = NONE
   val _ =
diff -r b9331caf92c3 -r 5399dfe9141c src/HOL/ex/veriT_Preprocessing.thy
--- a/src/HOL/ex/veriT_Preprocessing.thy	Wed Sep 29 11:55:09 2021 +0200
+++ b/src/HOL/ex/veriT_Preprocessing.thy	Wed Sep 29 18:21:22 2021 +0200
@@ -42,12 +42,10 @@
     val tuple_T = fastype_of tuple_t;
 
     val lambda_t = HOLogic.tupled_lambda tuple_t (list_comb (p, ts));
-    val lambda_T = fastype_of lambda_t;
 
     val left_prems = map2 (curry Ctr_Sugar_Util.mk_Trueprop_eq) ts us;
     val right_prem = Ctr_Sugar_Util.mk_Trueprop_eq (list_comb (p, us), q);
-    val concl = Ctr_Sugar_Util.mk_Trueprop_eq
-      (Const (\<^const_name>\<open>Let\<close>, tuple_T --> lambda_T --> B) $ tuple_t $ lambda_t, q);
+    val concl = Ctr_Sugar_Util.mk_Trueprop_eq (\<^Const>\<open>Let tuple_T B for tuple_t lambda_t\<close>, q);
 
     val goal = Logic.list_implies (left_prems @ [right_prem], concl);
     val vars = Variable.add_free_names ctxt goal [];
@@ -82,8 +80,8 @@
 
 fun lambda_count (Abs (_, _, t)) = lambda_count t + 1
   | lambda_count ((t as Abs _) $ _) = lambda_count t - 1
-  | lambda_count ((t as Const (\<^const_name>\<open>case_prod\<close>, _) $ _) $ _) = lambda_count t - 1
-  | lambda_count (Const (\<^const_name>\<open>case_prod\<close>, _) $ t) = lambda_count t - 1
+  | lambda_count ((t as \<^Const_>\<open>case_prod _ _ _\<close> $ _) $ _) = lambda_count t - 1
+  | lambda_count \<^Const_>\<open>case_prod _ _ _ for t\<close> = lambda_count t - 1
   | lambda_count _ = 0;
 
 fun zoom apply =
@@ -96,20 +94,16 @@
         let val (t', u') = zo 1 (T :: bound_Ts) (t, u) in
           (t' $ arg, u')
         end
-      | zo 0 bound_Ts ((t as Const (\<^const_name>\<open>case_prod\<close>, _) $ _) $ arg, u) =
+      | zo 0 bound_Ts ((t as \<^Const_>\<open>case_prod _ _ _\<close> $ _) $ arg, u) =
         let val (t', u') = zo 1 bound_Ts (t, u) in
           (t' $ arg, u')
         end
       | zo 0 bound_Ts tu = apply bound_Ts tu
-      | zo n bound_Ts (Const (\<^const_name>\<open>case_prod\<close>,
-          Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>fun\<close>, [A, Type (\<^type_name>\<open>fun\<close>, [B, _])]),
-            Type (\<^type_name>\<open>fun\<close>, [AB, _])])) $ t, u) =
+      | zo n bound_Ts (\<^Const_>\<open>case_prod A B _ for t\<close>, u) =
         let
           val (t', u') = zo (n + 1) bound_Ts (t, u);
           val C = range_type (range_type (fastype_of t'));
-        in
-          (Const (\<^const_name>\<open>case_prod\<close>, (A --> B --> C) --> AB --> C) $ t', u')
-        end
+        in (\<^Const>\<open>case_prod A B C for t'\<close>, u') end
       | zo n bound_Ts (Abs (s, T, t), u) =
         let val (t', u') = zo (n - 1) (T :: bound_Ts) (t, u) in
           (Abs (s, T, t'), u')
@@ -130,26 +124,26 @@
 
 fun apply_Bind (lhs, rhs) =
   (case (lhs, rhs) of
-    (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, T, t), Const (\<^const_name>\<open>All\<close>, _) $ Abs (s, U, u)) =>
+    (\<^Const_>\<open>All _ for \<open>Abs (_, T, t)\<close>\<close>, \<^Const_>\<open>All _ for \<open>Abs (s, U, u)\<close>\<close>) =>
     (Abs (s, T, t), Abs (s, U, u))
-  | (Const (\<^const_name>\<open>Ex\<close>, _) $ t, Const (\<^const_name>\<open>Ex\<close>, _) $ u) => (t, u)
+  | (\<^Const_>\<open>Ex _ for t\<close>, \<^Const_>\<open>Ex _ for u\<close>) => (t, u)
   | _ => raise TERM ("apply_Bind", [lhs, rhs]));
 
 fun apply_Sko_Ex (lhs, rhs) =
   (case lhs of
-    Const (\<^const_name>\<open>Ex\<close>, _) $ (t as Abs (_, T, _)) =>
+    \<^Const_>\<open>Ex _ for \<open>t as Abs (_, T, _)\<close>\<close> =>
     (t $ (HOLogic.choice_const T $ t), rhs)
   | _ => raise TERM ("apply_Sko_Ex", [lhs]));
 
 fun apply_Sko_All (lhs, rhs) =
   (case lhs of
-    Const (\<^const_name>\<open>All\<close>, _) $ (t as Abs (s, T, body)) =>
+    \<^Const_>\<open>All _ for \<open>t as Abs (s, T, body)\<close>\<close> =>
     (t $ (HOLogic.choice_const T $ Abs (s, T, HOLogic.mk_not body)), rhs)
   | _ => raise TERM ("apply_Sko_All", [lhs]));
 
 fun apply_Let_left ts j (lhs, _) =
   (case lhs of
-    Const (\<^const_name>\<open>Let\<close>, _) $ t $ _ =>
+    \<^Const_>\<open>Let _ _ for t _\<close> =>
     let val ts0 = HOLogic.strip_tuple t in
       (nth ts0 j, nth ts j)
     end
@@ -158,7 +152,7 @@
 fun apply_Let_right ts bound_Ts (lhs, rhs) =
   let val t' = mk_tuple1 bound_Ts ts in
     (case lhs of
-      Const (\<^const_name>\<open>Let\<close>, _) $ _ $ u => (u $ t', rhs)
+      \<^Const_>\<open>Let _ _ for _ u\<close> => (u $ t', rhs)
     | _ => raise TERM ("apply_Let_right", [lhs, rhs]))
   end;