--- 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). *)