diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/simplifier.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -171,7 +171,7 @@
 
 (* get simprocs *)
 
-fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt) #> #1;
+fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
 val the_simproc = Name_Space.get o get_simprocs;
 
 val _ =
@@ -202,14 +202,12 @@
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
       let
-        val naming = Proof_Context.target_naming_of context;
         val b' = Morphism.binding phi b;
         val simproc' = transform_simproc phi simproc;
       in
         context
         |> Data.map (fn (ss, tab) =>
-          (ss addsimprocs [simproc'],
-            #2 (Name_Space.define (Context.proof_of context) true naming (b', simproc') tab)))
+          (ss addsimprocs [simproc'], #2 (Name_Space.define context true (b', simproc') tab)))
       end)
   end;