added safe_mk_meta_eq;
authorwenzelm
Mon Sep 04 21:19:27 2000 +0200 (2000-09-04)
changeset 98322092298f7421
parent 9831 9b883c416aef
child 9833 193dc80eaee9
added safe_mk_meta_eq;
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Mon Sep 04 21:19:07 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Mon Sep 04 21:19:27 2000 +0200
     1.3 @@ -76,6 +76,7 @@
     1.4  (*Make meta-equalities.  The operator below is Trueprop*)
     1.5  
     1.6  fun mk_meta_eq r = r RS eq_reflection;
     1.7 +fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
     1.8  
     1.9  val Eq_TrueI  = mk_meta_eq(prover  "P --> (P = True)"  RS mp);
    1.10  val Eq_FalseI = mk_meta_eq(prover "~P --> (P = False)" RS mp);