src/FOL/simpdata.ML
changeset 32155 e2bf2f73b0c8
parent 32149 ef59550a55d3
child 32177 bc02c5bfcb5b
     1.1 --- a/src/FOL/simpdata.ML	Thu Jul 23 22:20:37 2009 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Jul 23 23:12:21 2009 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4  
     1.5  (*No simprules, but basic infastructure for simplification*)
     1.6  val FOL_basic_ss =
     1.7 -  Simplifier.theory_context (the_context ()) empty_ss
     1.8 +  Simplifier.theory_context @{theory} empty_ss
     1.9    setsubgoaler asm_simp_tac
    1.10    setSSolver (mk_solver "FOL safe" safe_solver)
    1.11    setSolver (mk_solver "FOL unsafe" unsafe_solver)