src/HOL/simpdata.ML

     |   _$(Const("op =",_)$_$_) => mk_meta_eq th
     |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
     |   _                       => 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 =
   standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
   handle THM _ =>

                    | None => [th])
               | _ => [th])
          | _ => [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];
 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;