added safe_mk_meta_eq;

--- a/src/HOL/simpdata.ML	Mon Sep 04 21:19:07 2000 +0200
+++ b/src/HOL/simpdata.ML	Mon Sep 04 21:19:27 2000 +0200
@@ -76,6 +76,7 @@
 (*Make meta-equalities.  The operator below is Trueprop*)
 
 fun mk_meta_eq r = r RS eq_reflection;
+fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
 
 val Eq_TrueI  = mk_meta_eq(prover  "P --> (P = True)"  RS mp);
 val Eq_FalseI = mk_meta_eq(prover "~P --> (P = False)" RS mp);