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