# HG changeset patch
# User wenzelm
# Date 1635444577 -7200
# Node ID 98e7930e6d15994cf35cd3d636a0995673654783
# Parent  87fc10f5826c32c1985510f502e9cb752edf53d3
clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic;

diff -r 87fc10f5826c -r 98e7930e6d15 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Oct 28 20:06:29 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Oct 28 20:09:37 2021 +0200
@@ -101,13 +101,12 @@
 
 (* INFERENCE RULE: ASSUME *)
 
-fun inst_excluded_middle i_atom =
-  @{lemma "P \<Longrightarrow> \<not> P \<Longrightarrow> False" by (rule notE)}
-  |> instantiate_normalize (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, i_atom)])
+fun excluded_middle P =
+  \<^instantiate>\<open>P in lemma (open) \<open>P \<Longrightarrow> \<not> P \<Longrightarrow> False\<close> by (rule notE)\<close>
 
 fun assume_inference ctxt type_enc concealed sym_tab atom =
   singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)
-  |> Thm.cterm_of ctxt |> inst_excluded_middle
+  |> Thm.cterm_of ctxt |> excluded_middle
 
 
 (* INFERENCE RULE: INSTANTIATE (SUBST). *)
diff -r 87fc10f5826c -r 98e7930e6d15 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Thu Oct 28 20:06:29 2021 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Thu Oct 28 20:09:37 2021 +0200
@@ -60,8 +60,8 @@
 fun is_nat t = (fastype_of1 t = HOLogic.natT);
 
 fun mk_nat_thm thy t =
-  let val ct = Thm.global_cterm_of thy t
-  in Drule.instantiate_normalize (TVars.empty, Vars.make [(\<^var>\<open>?n::nat\<close>, ct)]) @{thm le0} end;
+  \<^instantiate>\<open>n = \<open>Thm.global_cterm_of thy t\<close> in
+    lemma (open) \<open>0 \<le> n\<close> for n :: nat by (rule le0)\<close>;
 
 end;