src/Tools/Code/code_runtime.ML

--- a/src/Tools/Code/code_runtime.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -51,14 +51,14 @@
 
 datatype truth = Holds;
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
   #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
     [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
   #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
     [(target, SOME (Code_Printer.plain_const_syntax s_Holds))]))
   #> Code_Target.add_reserved target this
-  #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
+  #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
        (*avoid further pervasive infix names*)
 
 val trace = Unsynchronized.ref false;
@@ -345,10 +345,9 @@
 
 (** Isar setup **)
 
-val _ =
-  Context.>> (Context.map_theory
-    (ML_Context.add_antiq @{binding code}
-      (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context))));
+val _ = Theory.setup
+  (ML_Context.add_antiq @{binding code}
+    (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context)));
 
 local
 
@@ -387,7 +386,7 @@
 fun notify_val (string, value) = 
   let
     val _ = #enterVal ML_Env.name_space (string, value);
-    val _ = Context.>> ((Context.map_theory o Loaded_Values.map) (insert (op =) string));
+    val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
   in () end;
 
 fun abort _ = error "Only value bindings allowed.";