# HG changeset patch
# User wenzelm
# Date 968095167 -7200
# Node ID 2092298f74218d9b1b185b98020dd40fb60e1c7a
# Parent  9b883c416aef43fe44f6b798ae454b60ac15749f
added safe_mk_meta_eq;

diff -r 9b883c416aef -r 2092298f7421 src/HOL/simpdata.ML
--- 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);