re-added refl in safe_solver
authoroheimb
Mon Aug 16 17:24:28 1999 +0200 (1999-08-16)
changeset 721308a354bbc34c
parent 7212 1ad29e7d917b
child 7214 381d6987f68d
re-added refl in safe_solver
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Mon Aug 16 16:44:47 1999 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Mon Aug 16 17:24:28 1999 +0200
     1.3 @@ -429,10 +429,10 @@
     1.4  
     1.5  fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
     1.6  
     1.7 -fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
     1.8 -				 atac, etac FalseE];
     1.9 +fun unsafe_solver prems = FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems),
    1.10 +				 atac         ,       etac  FalseE ];
    1.11  (*No premature instantiation of variables during simplification*)
    1.12 -fun   safe_solver prems = FIRST'[match_tac (reflexive_thm::TrueI::prems),
    1.13 +fun   safe_solver prems = FIRST'[  match_tac(reflexive_thm::TrueI::refl::prems),
    1.14  				 eq_assume_tac, ematch_tac [FalseE]];
    1.15  
    1.16  val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac