# HG changeset patch
# User wenzelm
# Date 1635720067 -3600
# Node ID b31683a544cf147311943d15dd54c7ef1df3d29d
# Parent  546444db8173d6636ed6236e53bc8047571aefb0
clarified antiquotations;

diff -r 546444db8173 -r b31683a544cf src/HOL/Tools/Argo/argo_tactic.ML
--- a/src/HOL/Tools/Argo/argo_tactic.ML	Sun Oct 31 23:15:46 2021 +0100
+++ b/src/HOL/Tools/Argo/argo_tactic.ML	Sun Oct 31 23:41:07 2021 +0100
@@ -302,9 +302,6 @@
   let val cprop = as_prop ct
   in Thm.implies_intr cprop (f (Thm.assume cprop)) end
 
-fun instantiate cv ct =
-  Thm.instantiate (TVars.empty, Vars.make [(Term.dest_Var (Thm.term_of cv), ct)])
-
 
 (* proof replay for tautologies *)
 
@@ -517,8 +514,6 @@
 
 (* proof replay for unit resolution *)
 
-val unit_rule = @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not>P \<Longrightarrow> False) \<Longrightarrow> False" by fast}
-val unit_rule_var = Thm.dest_arg (Thm.dest_arg1 (Thm.cprem_of unit_rule 1))
 val bogus_ct = \<^cterm>\<open>True\<close>
 
 fun replay_unit_res lit (pthm, plits) (nthm, nlits) =
@@ -527,8 +522,8 @@
     val nlit = the (AList.lookup (op =) nlits (~lit))
     val prune = Ord_List.remove lit_ord (lit, bogus_ct)
   in
-    unit_rule
-    |> instantiate unit_rule_var (Thm.dest_arg plit)
+    \<^instantiate>\<open>P = \<open>Thm.dest_arg plit\<close> in
+      lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not>P \<Longrightarrow> False) \<Longrightarrow> False" by fast\<close>
     |> Thm.elim_implies (Thm.implies_intr plit pthm)
     |> Thm.elim_implies (Thm.implies_intr nlit nthm)
     |> rpair (Ord_List.union lit_ord (prune nlits) (prune plits))
@@ -553,10 +548,8 @@
 
 (* proof replay for reflexivity *)
 
-val refl_rule = @{thm refl}
-val refl_rule_var = Thm.dest_arg1 (Thm.dest_arg (Thm.cprop_of refl_rule))
-
-fun replay_refl ct = Thm.instantiate (Thm.match (refl_rule_var, ct)) refl_rule
+fun replay_refl x =
+  \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x in lemma \<open>x = x\<close> by (rule refl)\<close>
 
 
 (* proof replay for symmetry *)
@@ -663,13 +656,15 @@
 
 (* normalizing goals *)
 
+fun instantiate v ct = Thm.instantiate (TVars.empty, Vars.make [(v, ct)])
+
 fun instantiate_elim_rule thm =
-  let val ct = Drule.strip_imp_concl (Thm.cprop_of thm)
+  let
+    val ct = Drule.strip_imp_concl (Thm.cprop_of thm)
   in
     (case Thm.term_of ct of
-      \<^Const_>\<open>Trueprop for \<open>Var (_, \<^Type>\<open>bool\<close>)\<close>\<close> =>
-        instantiate (Thm.dest_arg ct) \<^cterm>\<open>False\<close> thm
-    | Var _ => instantiate ct \<^cprop>\<open>False\<close> thm
+      \<^Const_>\<open>Trueprop for \<open>Var (v as (_, \<^Type>\<open>bool\<close>))\<close>\<close> => instantiate v \<^cterm>\<open>False\<close> thm
+    | Var v => instantiate v \<^cprop>\<open>False\<close> thm
     | _ => thm)
   end