# HG changeset patch
# User wenzelm
# Date 1723285577 -7200
# Node ID fd69f98e218284dc0b3327f5db96259464ef070c
# Parent  c5c9b4470d06b64dfb1131dee49d133d42f5656e
tuned: more antiquotations;

diff -r c5c9b4470d06 -r fd69f98e2182 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 10 12:12:53 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 10 12:26:17 2024 +0200
@@ -550,32 +550,9 @@
 
 (** The General Shape of the Lifting Procedure **)
 
-(* - A is the original raw theorem
-   - B is the regularized theorem
-   - C is the rep/abs injected version of B
-   - D is the lifted theorem
-
-   - 1st prem is the regularization step
-   - 2nd prem is the rep/abs injection step
-   - 3rd prem is the cleaning part
-
-   the Quot_True premise in 2nd records the lifted theorem
-*)
-val procedure_thm =
-  @{lemma  "\<lbrakk>A;
-              A \<longrightarrow> B;
-              Quot_True D \<Longrightarrow> B = C;
-              C = D\<rbrakk> \<Longrightarrow> D"
-      by (simp add: Quot_True_def)}
-
 (* in case of partial equivalence relations, this form of the 
    procedure theorem results in solvable proof obligations 
 *)
-val partiality_procedure_thm =
-  @{lemma  "[|B; 
-              Quot_True D ==> B = C;
-              C = D|] ==> D"
-      by (simp add: Quot_True_def)}
 
 fun lift_match_error ctxt msg rtrm qtrm =
   let
@@ -596,11 +573,24 @@
     val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   in
-    Thm.instantiate' []
-      [SOME (Thm.cterm_of ctxt rtrm'),
-       SOME (Thm.cterm_of ctxt reg_goal),
-       NONE,
-       SOME (Thm.cterm_of ctxt inj_goal)] procedure_thm
+    (* - A is the original raw theorem
+       - B is the regularized theorem
+       - C is the rep/abs injected version of B
+       - D is the lifted theorem
+
+       - 1st prem is the regularization step
+       - 2nd prem is the rep/abs injection step
+       - 3rd prem is the cleaning part
+
+       the Quot_True premise in 2nd records the lifted theorem
+    *)
+    \<^instantiate>\<open>
+      A = \<open>Thm.cterm_of ctxt rtrm'\<close> and
+      B = \<open>Thm.cterm_of ctxt reg_goal\<close> and
+      C = \<open>Thm.cterm_of ctxt inj_goal\<close>
+    in
+      lemma (schematic) "A \<Longrightarrow> A \<longrightarrow> B \<Longrightarrow> (Quot_True D \<Longrightarrow> B = C) \<Longrightarrow> C = D \<Longrightarrow> D"
+        by (simp add: Quot_True_def)\<close>
   end
 
 
@@ -655,10 +645,12 @@
     val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   in
-    Thm.instantiate' []
-      [SOME (Thm.cterm_of ctxt reg_goal),
-       NONE,
-       SOME (Thm.cterm_of ctxt inj_goal)] partiality_procedure_thm
+    \<^instantiate>\<open>
+      B = \<open>Thm.cterm_of ctxt reg_goal\<close> and
+      C = \<open>Thm.cterm_of ctxt inj_goal\<close>
+    in
+      lemma (schematic) "B \<Longrightarrow> (Quot_True D \<Longrightarrow> B = C) \<Longrightarrow> C = D \<Longrightarrow> D"
+        by (simp add: Quot_True_def)\<close>
   end