# HG changeset patch
# User berghofe
# Date 1001690386 -7200
# Node ID 8a45c7abef0406dd314cf153386ef23458b9ed7e
# Parent  9c95b6a76e158906460f0c9070085725098aff7d
mksimps and mk_eq_True no longer raise THM exception.

diff -r 9c95b6a76e15 -r 8a45c7abef04 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Sep 28 16:45:03 2001 +0200
+++ b/src/HOL/simpdata.ML	Fri Sep 28 17:19:46 2001 +0200
@@ -38,7 +38,8 @@
     |   _                       => th RS Eq_TrueI;
 (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
 
-fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI);
+fun mk_eq_True r =
+  Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None;
 
 (*Congruence rules for = (instead of ==)*)
 fun mk_meta_cong rl =
@@ -352,7 +353,8 @@
          | _ => [th])
   in atoms end;
 
-fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe);
+fun mksimps pairs =
+  (mapfilter (try mk_eq) o mk_atomize pairs o forall_elim_vars_safe);
 
 fun unsafe_solver_tac prems =
   FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];