# HG changeset patch
# User wenzelm
# Date 1565613595 -7200
# Node ID 23168cbe0ef8828e9792b9a78cd5a1fb5b2e264d
# Parent  06a62b29085e041171c424ac1f7a0af2628e7981
tuned;

diff -r 06a62b29085e -r 23168cbe0ef8 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Aug 12 11:16:10 2019 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Aug 12 14:39:55 2019 +0200
@@ -101,20 +101,20 @@
 
 (* INFERENCE RULE: ASSUME *)
 
-val EXCLUDED_MIDDLE = @{lemma "P \<Longrightarrow> \<not> P \<Longrightarrow> False" by (rule notE)}
-
-fun inst_excluded_middle ctxt i_atom =
-  let val [vx] = Term.add_vars (Thm.prop_of EXCLUDED_MIDDLE) []
-  in infer_instantiate_types ctxt [(vx, Thm.cterm_of ctxt i_atom)] EXCLUDED_MIDDLE end
+fun inst_excluded_middle i_atom =
+  @{lemma "P \<Longrightarrow> \<not> P \<Longrightarrow> False" by (rule notE)}
+  |> instantiate_normalize ([], [((("P", 0), \<^typ>\<open>bool\<close>), i_atom)])
 
 fun assume_inference ctxt type_enc concealed sym_tab atom =
-  inst_excluded_middle ctxt
-    (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom))
+  singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)
+  |> Thm.cterm_of ctxt |> inst_excluded_middle
+
 
-(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
-   to reconstruct them admits new possibilities of errors, e.g. concerning
-   sorts. Instead we try to arrange that new TVars are distinct and that types
-   can be inferred from terms. *)
+(* INFERENCE RULE: INSTANTIATE (SUBST). *)
+
+(*Type instantiations are ignored. Trying to reconstruct them admits new
+  possibilities of errors, e.g. concerning sorts. Instead we try to arrange
+  hat new TVars are distinct and that types can be inferred from terms.*)
 
 fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
   let
@@ -298,7 +298,7 @@
 
 (* INFERENCE RULE: REFL *)
 
-val REFL_THM = Thm.incr_indexes 2 @{lemma "t \<noteq> t \<Longrightarrow> False" by (drule notE) (rule refl)}
+val REFL_THM = Thm.incr_indexes 2 @{lemma "x \<noteq> x \<Longrightarrow> False" by (drule notE) (rule refl)}
 
 val [refl_x] = Term.add_vars (Thm.prop_of REFL_THM) [];
 val refl_idx = 1 + Thm.maxidx_of REFL_THM;