# HG changeset patch
# User wenzelm
# Date 1737667240 -3600
# Node ID 4741b78bbc7933849e28ef3e6e34bed83269aca9
# Parent  326ecfc079a6348434d8578232da9396e377a34e
more antiquotations;

diff -r 326ecfc079a6 -r 4741b78bbc79 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Thu Jan 23 22:19:30 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Thu Jan 23 22:20:40 2025 +0100
@@ -59,7 +59,7 @@
   let
     val (t, u) = Thm.dest_equals (Thm.cprop_of th)
     val A = Thm.ctyp_of_cterm t
-    val rl = Thm.instantiate' [SOME A] [SOME t, SOME u] @{thm meta_eq_to_obj_eq}
+    val rl = \<^instantiate>\<open>(no_beta) 'a = A and t and u in lemma \<open>t \<equiv> u \<Longrightarrow> t = u\<close> by simp\<close>
   in
     Thm.implies_elim rl th
   end
@@ -68,7 +68,7 @@
   let
     val (t, u) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_of th))
     val A = Thm.ctyp_of_cterm t
-    val rl = Thm.instantiate' [SOME A] [SOME t, SOME u] @{thm eq_reflection}
+    val rl = \<^instantiate>\<open>(no_beta) 'a = A and t and u in lemma \<open>t = u \<Longrightarrow> t \<equiv> u\<close> by simp\<close>
   in
     Thm.implies_elim rl th
   end
@@ -78,7 +78,7 @@
 fun eq_mp th1 th2 =
   let
     val (Q, P) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_of th1))
-    val rl = Thm.instantiate' [] [SOME Q, SOME P] @{thm iffD1}
+    val rl = \<^instantiate>\<open>(no_beta) P and Q in lemma \<open>Q = P \<Longrightarrow> Q \<Longrightarrow> P\<close> by (fact iffD1)\<close>
   in
     Thm.implies_elim (Thm.implies_elim rl th1) th2
   end
@@ -96,16 +96,18 @@
     val th1' = Thm.implies_intr P th1
     val th2' = Thm.implies_intr Q th2
     val rl =
-      Thm.instantiate' [] [SOME (HOLogic.dest_judgment Q), SOME (HOLogic.dest_judgment P)]
-        @{thm iffI}
+      \<^instantiate>\<open>(no_beta)
+          P = \<open>HOLogic.dest_judgment P\<close> and
+          Q = \<open>HOLogic.dest_judgment Q\<close>
+        in lemma \<open>(P \<Longrightarrow> Q) \<Longrightarrow> (Q \<Longrightarrow> P) \<Longrightarrow> Q = P\<close> by (rule iffI)\<close>
   in
-    Thm.implies_elim (Thm.implies_elim rl th2') th1'
+    Thm.implies_elim (Thm.implies_elim rl th1') th2'
   end
 
 fun conj1 th =
   let
     val (P, Q) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_of th))
-    val rl = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct1}
+    val rl = \<^instantiate>\<open>(no_beta) P and Q in lemma \<open>P \<and> Q \<Longrightarrow> P\<close> by (fact conjunct1)\<close>
   in
     Thm.implies_elim rl th
   end
@@ -113,14 +115,13 @@
 fun conj2 th =
   let
     val (P, Q) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_of th))
-    val rl = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct2}
+    val rl = \<^instantiate>\<open>(no_beta) P and Q in lemma \<open>P \<and> Q \<Longrightarrow> Q\<close> by (fact conjunct2)\<close>
   in
     Thm.implies_elim rl th
   end
 
 fun refl t =
-  let val A = Thm.ctyp_of_cterm t
-  in Thm.instantiate' [SOME A] [SOME t] @{thm refl} end
+  \<^instantiate>\<open>(no_beta) 'a = \<open>Thm.ctyp_of_cterm t\<close> and t in lemma \<open>t = t\<close> by (fact refl)\<close>
 
 fun abs x th =
   to_meta_eq th |> Thm.abstract_rule (Term.term_name (Thm.term_of x)) x |> to_obj_eq
@@ -202,10 +203,10 @@
 (* type definitions *)
 
 fun typedef_hol2hollight A B rep abs pred a r =
-  Thm.instantiate' [SOME A, SOME B] [SOME rep, SOME abs, SOME pred, SOME a, SOME r]
-    @{lemma "type_definition Rep Abs (Collect P) \<Longrightarrow> Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
+  \<^instantiate>\<open>(no_beta) 'a = A and 'b = B and Rep = rep and Abs = abs and P = pred and a and r
+    in lemma "type_definition Rep Abs (Collect P) \<Longrightarrow> Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
         by (metis type_definition.Rep_inverse type_definition.Abs_inverse
-              type_definition.Rep mem_Collect_eq)}
+              type_definition.Rep mem_Collect_eq)\<close>
 
 fun typedef_hollight th =
   let
@@ -224,8 +225,8 @@
 
     val T = Thm.ctyp_of_cterm t
     val nonempty =
-      Thm.instantiate' [SOME T] [SOME P, SOME t]
-        @{lemma "P t \<Longrightarrow> \<exists>x. x \<in> Collect P" by auto}
+      \<^instantiate>\<open>(no_beta) 'a = T and P and t
+        in lemma "P t \<Longrightarrow> \<exists>x. x \<in> Collect P" by auto\<close>
       |> Thm.elim_implies witness
     val \<^Const_>\<open>Trueprop for \<^Const_>\<open>Ex _ for \<open>Abs (_, _, \<^Const_>\<open>Set.member _ for _ set\<close>)\<close>\<close>\<close> =
       Thm.concl_of nonempty