diff -r 7a6c4d60a913 -r 62c397c17d18 src/FOL/simpdata.ML
--- 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)