mksimps and mk_eq_True no longer raise THM exception.
authorberghofe
Fri Sep 28 17:19:46 2001 +0200 (2001-09-28)
changeset 116248a45c7abef04
parent 11623 9c95b6a76e15
child 11625 74cdf24724ea
mksimps and mk_eq_True no longer raise THM exception.
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Fri Sep 28 16:45:03 2001 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Sep 28 17:19:46 2001 +0200
     1.3 @@ -38,7 +38,8 @@
     1.4      |   _                       => th RS Eq_TrueI;
     1.5  (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
     1.6  
     1.7 -fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI);
     1.8 +fun mk_eq_True r =
     1.9 +  Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None;
    1.10  
    1.11  (*Congruence rules for = (instead of ==)*)
    1.12  fun mk_meta_cong rl =
    1.13 @@ -352,7 +353,8 @@
    1.14           | _ => [th])
    1.15    in atoms end;
    1.16  
    1.17 -fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe);
    1.18 +fun mksimps pairs =
    1.19 +  (mapfilter (try mk_eq) o mk_atomize pairs o forall_elim_vars_safe);
    1.20  
    1.21  fun unsafe_solver_tac prems =
    1.22    FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];