changeset 32155 | e2bf2f73b0c8 |
parent 32091 | 30e2ffbba718 |
child 32957 | 675c0c7e6a37 |
--- a/src/Sequents/simpdata.ML Thu Jul 23 22:20:37 2009 +0200 +++ b/src/Sequents/simpdata.ML Thu Jul 23 23:12:21 2009 +0200 @@ -68,7 +68,7 @@ (*No simprules, but basic infrastructure for simplification*) val LK_basic_ss = - Simplifier.theory_context (the_context ()) empty_ss + Simplifier.theory_context @{theory} empty_ss setsubgoaler asm_simp_tac setSSolver (mk_solver "safe" safe_solver) setSolver (mk_solver "unsafe" unsafe_solver)