diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/Sequents/simpdata.ML
--- 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)