changeset 17892 | 62c397c17d18 |
parent 17876 | b9c92f384109 |
child 21426 | 87ac12bed1ab |
--- a/src/Sequents/simpdata.ML Tue Oct 18 17:59:24 2005 +0200 +++ b/src/Sequents/simpdata.ML Tue Oct 18 17:59:25 2005 +0200 @@ -235,7 +235,8 @@ (*No simprules, but basic infrastructure for simplification*) val LK_basic_ss = - empty_ss setsubgoaler asm_simp_tac + Simplifier.theory_context (the_context ()) empty_ss + setsubgoaler asm_simp_tac setSSolver (mk_solver "safe" safe_solver) setSolver (mk_solver "unsafe" unsafe_solver) setmksimps (map mk_meta_eq o atomize o gen_all)