properly inlined @{lemma} antiqutations -- might also reduce proof terms a bit;

--- a/src/HOL/Tools/metis_tools.ML	Sat Nov 14 19:56:18 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Sun Nov 15 00:23:26 2009 +0100
@@ -28,10 +28,10 @@
 (* ------------------------------------------------------------------------- *)
 (* Useful Theorems                                                           *)
 (* ------------------------------------------------------------------------- *)
-val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate @{context} [(("R", 0), "False")] notE);
-val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
-val subst_em  = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
-val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
+val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
+val REFL_THM = incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
+val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
+val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
 
 (* ------------------------------------------------------------------------- *)
 (* Useful Functions                                                          *)