# HG changeset patch
# User wenzelm
# Date 1635444389 -7200
# Node ID 87fc10f5826c32c1985510f502e9cb752edf53d3
# Parent  3ef6e38c9847cfcf2f720aa82a990ee877679dad
clarified antiquotations;

diff -r 3ef6e38c9847 -r 87fc10f5826c src/HOL/Meson.thy
--- a/src/HOL/Meson.thy	Thu Oct 28 20:05:18 2021 +0200
+++ b/src/HOL/Meson.thy	Thu Oct 28 20:06:29 2021 +0200
@@ -190,7 +190,6 @@
 unfolding skolem_def COMBK_def by (rule refl)
 
 lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
-lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
 
 
 subsection \<open>Meson package\<close>
@@ -204,6 +203,5 @@
     not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD
     disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI
     ext_cong_neq COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K
-    abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
-
+    abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I
 end
diff -r 3ef6e38c9847 -r 87fc10f5826c src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Oct 28 20:05:18 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Oct 28 20:06:29 2021 +0200
@@ -366,9 +366,9 @@
        th ctxt1
     val (cnf_ths, ctxt2) = clausify nnf_th
     fun intr_imp ct th =
-      Thm.instantiate
-        (TVars.empty, Vars.make [(\<^var>\<open>?i::nat\<close>, Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))])
-        (zero_var_indexes @{thm skolem_COMBK_D})
+      \<^instantiate>\<open>i = \<open>Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no)\<close> in
+        lemma (schematic) \<open>skolem (COMBK P i) \<Longrightarrow> P\<close> for i :: nat
+          by (rule iffD2 [OF skolem_COMBK_iff])\<close>
       RS Thm.implies_intr ct th
   in
     (opt |> Option.map (I #>> singleton (Variable.export ctxt2 ctxt0)
diff -r 3ef6e38c9847 -r 87fc10f5826c src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Oct 28 20:05:18 2021 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Oct 28 20:06:29 2021 +0200
@@ -205,16 +205,17 @@
   let
     val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
       handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
-    val inst = (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, P), (\<^var>\<open>?Q::bool\<close>, Q)]);
-  in Drule.implies_elim_list (Thm.instantiate inst @{thm conjI}) [thP, thQ] end;
+    val rule = \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q\<close> by (rule conjI)\<close>
+  in Drule.implies_elim_list rule [thP, thQ] end;
 
 fun conj_elim ctxt thPQ =
   let
     val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
       handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
-    val inst = (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, P), (\<^var>\<open>?Q::bool\<close>, Q)]);
-    val thP = Thm.implies_elim (Thm.instantiate inst @{thm conjunct1}) thPQ;
-    val thQ = Thm.implies_elim (Thm.instantiate inst @{thm conjunct2}) thPQ;
+    val thP =
+      Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> P\<close> by (rule conjunct1)\<close> thPQ;
+    val thQ =
+      Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> Q\<close> by (rule conjunct2)\<close> thPQ;
   in (thP, thQ) end;
 
 fun conj_elims ctxt th =
diff -r 3ef6e38c9847 -r 87fc10f5826c src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Oct 28 20:05:18 2021 +0200
+++ b/src/HOL/Tools/record.ML	Thu Oct 28 20:06:29 2021 +0200
@@ -1752,9 +1752,8 @@
         rewrite_rule ctxt
           [Axclass.unoverload ctxt (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
       fun mk_eq_refl ctxt =
-        @{thm equal_refl}
-        |> Thm.instantiate
-          (TVars.make [(\<^tvar>\<open>?'a::equal\<close>, Thm.ctyp_of ctxt (Logic.varifyT_global extT))], Vars.empty)
+        \<^instantiate>\<open>'a = \<open>Thm.ctyp_of ctxt (Logic.varifyT_global extT)\<close> in
+          lemma (schematic) \<open>equal_class.equal x x \<longleftrightarrow> True\<close> by (rule equal_refl)\<close>
         |> Axclass.unoverload ctxt;
       val ensure_random_record = ensure_sort_record (\<^sort>\<open>random\<close>, mk_random_eq);
       val ensure_exhaustive_record =
diff -r 3ef6e38c9847 -r 87fc10f5826c src/HOL/Tools/sat.ML
--- a/src/HOL/Tools/sat.ML	Thu Oct 28 20:05:18 2021 +0200
+++ b/src/HOL/Tools/sat.ML	Thu Oct 28 20:06:29 2021 +0200
@@ -70,9 +70,6 @@
 
 val counter = Unsynchronized.ref 0;
 
-val resolution_thm =
-  @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not> P \<Longrightarrow> False) \<Longrightarrow> False" by (rule case_split)}
-
 (* ------------------------------------------------------------------------- *)
 (* lit_ord: an order on integers that considers their absolute values only,  *)
 (*      thereby treating integers that represent the same atom (positively   *)
@@ -166,12 +163,13 @@
             val c1' = Thm.implies_intr hyp1 c1  (* Gamma1 |- hyp1 ==> False *)
             val c2' = Thm.implies_intr hyp2 c2  (* Gamma2 |- hyp2 ==> False *)
 
-            val res_thm =  (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
+            val res_thm =
               let
-                val cLit =
+                val P =
                   snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1))  (* strip Trueprop *)
               in
-                Thm.instantiate (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, cLit)]) resolution_thm
+                \<^instantiate>\<open>P in
+                  lemma \<open>(P \<Longrightarrow> False) \<Longrightarrow> (\<not> P \<Longrightarrow> False) \<Longrightarrow> False\<close> by (rule case_split)\<close>
               end
 
             val _ =