# HG changeset patch
# User wenzelm
# Date 1631390863 -7200
# Node ID 9a9326a072bb296cb4e8d4545ae7cde294cbec7c
# Parent  ee04dc00bf0a9cc5a651b6adabcc5bdf1a333d3d
more antiquotations;

diff -r ee04dc00bf0a -r 9a9326a072bb src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sat Sep 11 22:02:12 2021 +0200
+++ b/src/Provers/hypsubst.ML	Sat Sep 11 22:07:43 2021 +0200
@@ -112,8 +112,8 @@
             orelse exists (curry Logic.occs (Free f)) ts
         then (orient, true) else raise Match
       | check_free ts (orient, _) = (orient, false)
-    fun eq_var_aux k (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(_,_,t)) hs = eq_var_aux k t hs
-      | eq_var_aux k (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ A $ B) hs =
+    fun eq_var_aux k \<^Const_>\<open>Pure.all _ for \<open>Abs(_,_,t)\<close>\<close> hs = eq_var_aux k t hs
+      | eq_var_aux k \<^Const_>\<open>Pure.imp for A B\<close> hs =
               ((k, check_free (B :: hs) (inspect_pair bnd novars
                     (Data.dest_eq (Data.dest_Trueprop A))))
                handle TERM _ => eq_var_aux (k+1) B (A :: hs)
diff -r ee04dc00bf0a -r 9a9326a072bb src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Sat Sep 11 22:02:12 2021 +0200
+++ b/src/Provers/splitter.ML	Sat Sep 11 22:07:43 2021 +0200
@@ -57,7 +57,7 @@
 
 fun split_thm_info thm =
   (case Thm.concl_of (Data.mk_eq thm) of
-    Const(\<^const_name>\<open>Pure.eq\<close>, _) $ (Var _ $ t) $ c =>
+    \<^Const_>\<open>Pure.eq _ for \<open>Var _ $ t\<close> c\<close> =>
       (case strip_comb t of
         (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false)
       | _ => split_format_err ())
diff -r ee04dc00bf0a -r 9a9326a072bb src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Sep 11 22:02:12 2021 +0200
+++ b/src/Tools/induct.ML	Sat Sep 11 22:07:43 2021 +0200
@@ -665,16 +665,14 @@
 
 local
 
-fun goal_prefix k ((c as Const (\<^const_name>\<open>Pure.all\<close>, _)) $ Abs (a, T, B)) =
-      c $ Abs (a, T, goal_prefix k B)
+fun goal_prefix k ((c as \<^Const_>\<open>Pure.all _\<close>) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
   | goal_prefix 0 _ = Term.dummy_prop
-  | goal_prefix k ((c as Const (\<^const_name>\<open>Pure.imp\<close>, _)) $ A $ B) =
-      c $ A $ goal_prefix (k - 1) B
+  | goal_prefix k ((c as \<^Const_>\<open>Pure.imp\<close>) $ A $ B) = c $ A $ goal_prefix (k - 1) B
   | goal_prefix _ _ = Term.dummy_prop;
 
-fun goal_params k (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, B)) = goal_params k B + 1
+fun goal_params k \<^Const_>\<open>Pure.all _ for \<open>Abs (_, _, B)\<close>\<close> = goal_params k B + 1
   | goal_params 0 _ = 0
-  | goal_params k (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _ $ B) = goal_params (k - 1) B
+  | goal_params k \<^Const_>\<open>Pure.imp for _ B\<close> = goal_params (k - 1) B
   | goal_params _ _ = 0;
 
 fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
@@ -690,13 +688,11 @@
           [(#1 (dest_Var (head_of pred)), Thm.cterm_of ctxt (Logic.rlist_abs (xs, body))),
            (#1 (dest_Var (head_of arg)), Thm.cterm_of ctxt (Logic.rlist_abs (xs, v)))]);
 
-    fun goal_concl k xs (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (a, T, B)) =
-          goal_concl k ((a, T) :: xs) B
+    fun goal_concl k xs \<^Const_>\<open>Pure.all _ for \<open>Abs (a, T, B)\<close>\<close> = goal_concl k ((a, T) :: xs) B
       | goal_concl 0 xs B =
           if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
           else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B))
-      | goal_concl k xs (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _ $ B) =
-          goal_concl (k - 1) xs B
+      | goal_concl k xs \<^Const_>\<open>Pure.imp for _ B\<close> = goal_concl (k - 1) xs B
       | goal_concl _ _ _ = NONE;
   in
     (case goal_concl n [] goal of
diff -r ee04dc00bf0a -r 9a9326a072bb src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Sat Sep 11 22:02:12 2021 +0200
+++ b/src/Tools/misc_legacy.ML	Sat Sep 11 22:07:43 2021 +0200
@@ -124,9 +124,9 @@
     H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
   Main difference from strip_assums concerns parameters:
     it replaces the bound variables by free variables.  *)
-fun strip_context_aux (params, Hs, Const (\<^const_name>\<open>Pure.imp\<close>, _) $ H $ B) =
+fun strip_context_aux (params, Hs, \<^Const_>\<open>Pure.imp for H B\<close>) =
       strip_context_aux (params, H :: Hs, B)
-  | strip_context_aux (params, Hs, Const (\<^const_name>\<open>Pure.all\<close>,_) $ Abs (a, T, t)) =
+  | strip_context_aux (params, Hs, \<^Const_>\<open>Pure.all _ for \<open>Abs (a, T, t)\<close>\<close>) =
       let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
       in strip_context_aux ((b, T) :: params, Hs, u) end
   | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
diff -r ee04dc00bf0a -r 9a9326a072bb src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sat Sep 11 22:02:12 2021 +0200
+++ b/src/Tools/nbe.ML	Sat Sep 11 22:07:43 2021 +0200
@@ -589,7 +589,7 @@
 fun mk_equals ctxt lhs raw_rhs =
   let
     val ty = Thm.typ_of_cterm lhs;
-    val eq = Thm.cterm_of ctxt (Term.Const (\<^const_name>\<open>Pure.eq\<close>, ty --> ty --> propT));
+    val eq = Thm.cterm_of ctxt \<^Const>\<open>Pure.eq ty\<close>;
     val rhs = Thm.cterm_of ctxt raw_rhs;
   in Thm.mk_binop eq lhs rhs end;