# HG changeset patch
# User wenzelm
# Date 1565192628 -7200
# Node ID b203aaf373cf33ccdb07620c2aa0e50317d03a6c
# Parent  63333b6a22c0e8878964f955d1dd8b95c7862cd8
more compact proofterms;

diff -r 63333b6a22c0 -r b203aaf373cf src/HOL/Tools/Metis/metis_reconstruct.ML
--- 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