src/FOL/simpdata.ML
changeset 17892 62c397c17d18
parent 17875 d81094515061
child 18324 d1c4b1112e33
     1.1 --- a/src/FOL/simpdata.ML	Tue Oct 18 17:59:24 2005 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Tue Oct 18 17:59:25 2005 +0200
     1.3 @@ -330,7 +330,8 @@
     1.4                                   eq_assume_tac, ematch_tac [FalseE]];
     1.5  
     1.6  (*No simprules, but basic infastructure for simplification*)
     1.7 -val FOL_basic_ss = empty_ss
     1.8 +val FOL_basic_ss =
     1.9 +  Simplifier.theory_context (the_context ()) empty_ss
    1.10    setsubgoaler asm_simp_tac
    1.11    setSSolver (mk_solver "FOL safe" safe_solver)
    1.12    setSolver (mk_solver "FOL unsafe" unsafe_solver)