diff -r c1966f322105 -r d1650e3720fd src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/Pure/simplifier.ML	Mon Jun 27 16:53:31 2011 +0200
@@ -139,8 +139,9 @@
 fun map_simpset f = Context.proof_map (map_ss f);
 fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
 
-val _ = ML_Antiquote.value "simpset"
-  (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
+val _ = Context.>> (Context.map_theory
+  (ML_Antiquote.value (Binding.name "simpset")
+    (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())")));
 
 
 (* global simpset *)
@@ -158,15 +159,16 @@
 
 (* get simprocs *)
 
-fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt);
+fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt) #> #1;
 val the_simproc = Name_Space.get o get_simprocs;
 
 val _ =
-  ML_Antiquote.value "simproc"
-    (Args.context -- Scan.lift (Parse.position Args.name)
-      >> (fn (ctxt, name) =>
-        "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^
-          ML_Syntax.print_string (check_simproc ctxt name)));
+  Context.>> (Context.map_theory
+   (ML_Antiquote.value (Binding.name "simproc")
+      (Args.context -- Scan.lift (Parse.position Args.name)
+        >> (fn (ctxt, name) =>
+          "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^
+            ML_Syntax.print_string (check_simproc ctxt name)))));
 
 
 (* define simprocs *)