# HG changeset patch
# User wenzelm
# Date 1632250588 -7200
# Node ID f984d30cd0c3726367a714496d47ae2c90e3f792
# Parent  55007a70bd96c32c79b1e81a5a42e058514cb2dd
clarified antiquotations;

diff -r 55007a70bd96 -r f984d30cd0c3 src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Sep 21 20:56:23 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Tue Sep 21 20:56:28 2021 +0200
@@ -71,8 +71,7 @@
 fun conceal_old_skolem_terms i old_skolems t =
   if exists_Const (curry (op =) \<^const_name>\<open>Meson.skolem\<close> o fst) t then
     let
-      fun aux old_skolems
-             (t as (Const (\<^const_name>\<open>Meson.skolem\<close>, Type (_, [_, T])) $ _)) =
+      fun aux old_skolems (t as \<^Const_>\<open>Meson.skolem T for _\<close>) =
           let
             val (old_skolems, s) =
               if i = ~1 then
@@ -114,8 +113,8 @@
       if String.isPrefix lam_lifted_prefix s then
         (case AList.lookup (op =) lifted s of
           SOME t =>
-          Const (\<^const_name>\<open>Metis.lambda\<close>, dummyT)
-          $ map_types (map_type_tvar (K dummyT)) (reveal_lam_lifted lifted t)
+            \<^Const>\<open>Metis.lambda dummyT\<close> $
+              map_types (map_type_tvar (K dummyT)) (reveal_lam_lifted lifted t)
         | NONE => t)
       else
         t
@@ -190,7 +189,7 @@
     end
   | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula"
 
-fun eliminate_lam_wrappers (Const (\<^const_name>\<open>Metis.lambda\<close>, _) $ t) = eliminate_lam_wrappers t
+fun eliminate_lam_wrappers \<^Const_>\<open>Metis.lambda _ for t\<close> = eliminate_lam_wrappers t
   | eliminate_lam_wrappers (t $ u) = eliminate_lam_wrappers t $ eliminate_lam_wrappers u
   | eliminate_lam_wrappers (Abs (s, T, t)) = Abs (s, T, eliminate_lam_wrappers t)
   | eliminate_lam_wrappers t = t
diff -r 55007a70bd96 -r f984d30cd0c3 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Sep 21 20:56:23 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Sep 21 20:56:28 2021 +0200
@@ -221,10 +221,10 @@
       end
   end
 
-fun s_not (\<^const>\<open>Not\<close> $ t) = t
+fun s_not \<^Const_>\<open>Not for t\<close> = t
   | s_not t = HOLogic.mk_not t
-fun simp_not_not (\<^const>\<open>Trueprop\<close> $ t) = \<^const>\<open>Trueprop\<close> $ simp_not_not t
-  | simp_not_not (\<^const>\<open>Not\<close> $ t) = s_not (simp_not_not t)
+fun simp_not_not \<^Const_>\<open>Trueprop for t\<close> = \<^Const>\<open>Trueprop for \<open>simp_not_not t\<close>\<close>
+  | simp_not_not \<^Const_>\<open>Not for t\<close> = s_not (simp_not_not t)
   | simp_not_not t = t
 
 val normalize_literal = simp_not_not o Envir.eta_contract
@@ -414,7 +414,7 @@
 fun is_metis_literal_genuine (_, (s, _)) =
   not (String.isPrefix class_prefix (Metis_Name.toString s))
 fun is_isabelle_literal_genuine t =
-  (case t of _ $ (Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _) => false | _ => true)
+  (case t of _ $ \<^Const_>\<open>Meson.skolem _ for _\<close> => false | _ => true)
 
 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
 
@@ -660,11 +660,11 @@
 
       fun subst_info_of_prem subgoal_no prem =
         (case prem of
-          _ $ (Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ (_ $ t $ num)) =>
-          let val ax_no = HOLogic.dest_nat num in
-            (ax_no, (subgoal_no,
-                     match_term (nth axioms ax_no |> the |> snd, t)))
-          end
+          _ $ \<^Const_>\<open>Meson.skolem _ for \<open>_ $ t $ num\<close>\<close> =>
+            let val ax_no = HOLogic.dest_nat num in
+              (ax_no, (subgoal_no,
+                       match_term (nth axioms ax_no |> the |> snd, t)))
+            end
         | _ => raise TERM ("discharge_skolem_premises: Malformed premise", [prem]))
 
       fun cluster_of_var_name skolem s =
diff -r 55007a70bd96 -r f984d30cd0c3 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Sep 21 20:56:23 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Sep 21 20:56:28 2021 +0200
@@ -48,12 +48,12 @@
    "t => t". Type tag idempotence is also handled this way. *)
 fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
   (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
-    Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ t =>
+    \<^Const_>\<open>HOL.eq _ for _ t\<close> =>
       let
         val ct = Thm.cterm_of ctxt t
         val cT = Thm.ctyp_of_cterm ct
       in refl |> Thm.instantiate' [SOME cT] [SOME ct] end
-  | Const (\<^const_name>\<open>disj\<close>, _) $ t1 $ t2 =>
+  | \<^Const_>\<open>disj for t1 t2\<close> =>
       (if can HOLogic.dest_not t1 then t2 else t1)
       |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
   | _ => raise Fail "expected reflexive or trivial clause")
@@ -94,7 +94,7 @@
                     |> Thm.cterm_of ctxt
                     |> Conv.comb_conv (conv true ctxt))
               else Conv.abs_conv (conv false o snd) ctxt ct
-          | Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _ => Thm.reflexive ct
+          | \<^Const_>\<open>Meson.skolem _ for _\<close> => Thm.reflexive ct
           | _ => Conv.comb_conv (conv true ctxt) ct)
       val eq_th = conv true ctxt (Thm.cprop_of th)
       (* We replace the equation's left-hand side with a beta-equivalent term