--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 07 17:00:07 2019 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 07 17:43:48 2019 +0200
@@ -298,7 +298,7 @@
(* INFERENCE RULE: REFL *)
-val REFL_THM = Thm.incr_indexes 2 @{lemma "t \<noteq> t \<Longrightarrow> False" by simp}
+val REFL_THM = Thm.incr_indexes 2 @{lemma "t \<noteq> t \<Longrightarrow> False" by (drule notE) (rule refl)}
val refl_x = Thm.cterm_of \<^context> (Var (hd (Term.add_vars (Thm.prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
@@ -312,8 +312,8 @@
(* INFERENCE RULE: EQUALITY *)
-val subst_em = @{lemma "s = t \<Longrightarrow> P s \<Longrightarrow> \<not> P t \<Longrightarrow> False" by simp}
-val ssubst_em = @{lemma "s = t \<Longrightarrow> P t \<Longrightarrow> \<not> P s \<Longrightarrow> False" by simp}
+val subst_em = @{lemma "s = t \<Longrightarrow> P s \<Longrightarrow> \<not> P t \<Longrightarrow> False" by (erule notE) (erule subst)}
+val ssubst_em = @{lemma "s = t \<Longrightarrow> P t \<Longrightarrow> \<not> P s \<Longrightarrow> False" by (erule notE) (erule ssubst)}
fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr =
let val thy = Proof_Context.theory_of ctxt
@@ -523,7 +523,7 @@
infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) t_inst) th
end
-val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
+val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by assumption}
fun copy_prems_tac ctxt [] ns i =
if forall (curry (op =) 1) ns then all_tac else copy_prems_tac ctxt (rev ns) [] i