1.1 --- a/src/FOL/simpdata.ML	Wed Jun 29 20:39:41 2011 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Wed Jun 29 21:34:16 2011 +0200
     1.3 @@ -108,11 +108,12 @@
     1.4  
     1.5  val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
     1.6  
     1.7 -fun unsafe_solver ss = FIRST'[resolve_tac (triv_rls @ prems_of_ss ss),
     1.8 -                                 atac, etac @{thm FalseE}];
     1.9 +fun unsafe_solver ss =
    1.10 +  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), atac, etac @{thm FalseE}];
    1.11 +
    1.12  (*No premature instantiation of variables during simplification*)
    1.13 -fun safe_solver ss = FIRST'[match_tac (triv_rls @ prems_of_ss ss),
    1.14 -                                 eq_assume_tac, ematch_tac [@{thm FalseE}]];
    1.15 +fun safe_solver ss =
    1.16 +  FIRST' [match_tac (triv_rls @ Simplifier.prems_of ss), eq_assume_tac, ematch_tac @{thms FalseE}];
    1.17  
    1.18  (*No simprules, but basic infastructure for simplification*)
    1.19  val FOL_basic_ss =