src/HOL/simpdata.ML
changeset 7570 a9391550eea1
parent 7369 2d2110cda81e
child 7584 5be4bb8e4e3f
     1.1 --- a/src/HOL/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
     1.3 @@ -429,14 +429,18 @@
     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_tac prems =
    1.10 +  FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
    1.11 +val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
    1.12 +
    1.13  (*No premature instantiation of variables during simplification*)
    1.14 -fun   safe_solver prems = FIRST'[  match_tac(reflexive_thm::TrueI::refl::prems),
    1.15 -				 eq_assume_tac, ematch_tac [FalseE]];
    1.16 +fun safe_solver_tac prems =
    1.17 +  FIRST'[match_tac(reflexive_thm::TrueI::refl::prems),
    1.18 +         eq_assume_tac, ematch_tac [FalseE]];
    1.19 +val safe_solver = mk_solver "HOL safe" safe_solver_tac;
    1.20  
    1.21  val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
    1.22 -			    setSSolver   safe_solver
    1.23 +			    setSSolver safe_solver
    1.24  			    setSolver  unsafe_solver
    1.25  			    setmksimps (mksimps mksimps_pairs)
    1.26  			    setmkeqTrue mk_eq_True;