src/HOL/Tools/simpdata.ML

--- a/src/HOL/Tools/simpdata.ML	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/HOL/Tools/simpdata.ML	Thu Jul 23 23:12:21 2009 +0200
@@ -166,7 +166,7 @@
    ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
 
 val HOL_basic_ss =
-  Simplifier.theory_context (the_context ()) empty_ss
+  Simplifier.theory_context @{theory} empty_ss
     setsubgoaler asm_simp_tac
     setSSolver safe_solver
     setSolver unsafe_solver