src/Tools/Code/code_runtime.ML

--- a/src/Tools/Code/code_runtime.ML	Fri Aug 23 17:01:12 2013 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Aug 23 19:53:27 2013 +0200
@@ -247,12 +247,15 @@
 
 in
 
-fun ml_code_antiq raw_const background =
+fun ml_code_antiq context raw_const =
   let
-    val const = Code.check_const (Proof_Context.theory_of background) raw_const;
-    val is_first = is_first_occ background;
-    val background' = register_const const background;
-  in (print_code is_first const, background') end;
+    val ctxt = Context.the_proof context;
+    val thy = Proof_Context.theory_of ctxt;
+
+    val const = Code.check_const thy raw_const;
+    val is_first = is_first_occ ctxt;
+    val ctxt' = register_const const ctxt;
+  in (Context.Proof ctxt', print_code is_first const) end;
 
 end; (*local*)
 
@@ -344,7 +347,8 @@
 
 val _ =
   Context.>> (Context.map_theory
-    (ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq)));
+    (ML_Context.add_antiq @{binding code}
+      (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context))));
 
 local