# HG changeset patch
# User wenzelm
# Date 1635449332 -7200
# Node ID c496550dd2c26eed2edde2bd8a91a893b018c1f5
# Parent  6676bf1898526807812ba2087910291cd4ecd23e
clarified antiquotations;

diff -r 6676bf189852 -r c496550dd2c2 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Thu Oct 28 20:38:21 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Thu Oct 28 21:28:52 2021 +0200
@@ -47,7 +47,7 @@
           let
             val (a, A) = Thm.dest_comb S |>> Thm.dest_arg
             val cT = Thm.ctyp_of_cterm a
-            val ne = Thm.instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
+            val ne = \<^instantiate>\<open>'a = cT and a and A in lemma \<open>insert a A \<noteq> {}\<close> by simp\<close>
             val f = prove_finite cT (dest_set S)
          in (ne, f) end
 
@@ -112,7 +112,8 @@
     val rr = Thm.dest_arg r
     val thl  = prove_conj tabl (conjuncts rr) |> Drule.implies_intr_hyps
     val thr  = prove_conj tabr (conjuncts ll) |> Drule.implies_intr_hyps
-    val eqI = Thm.instantiate' [] [SOME ll, SOME rr] @{thm iffI}
+    val eqI =
+      \<^instantiate>\<open>P = ll and Q = rr in lemma \<open>(P \<Longrightarrow> Q) \<Longrightarrow> (Q \<Longrightarrow> P) \<Longrightarrow> P \<longleftrightarrow> Q\<close> by (rule iffI)\<close>
   in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
 
 fun contains x ct =