# HG changeset patch
# User wenzelm
# Date 1377282950 -7200
# Node ID a5e54d4d9081c6cc17f675a9a98dedffec1196e1
# Parent  96f7adb55d72d8a2b00bc573d0234c44308468a9
added Theory.setup convenience;

diff -r 96f7adb55d72 -r a5e54d4d9081 src/HOL/Import/import_data.ML
--- a/src/HOL/Import/import_data.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/HOL/Import/import_data.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -90,16 +90,16 @@
 val parser = Parse.name -- Scan.option (Parse.$$$ ":" |-- Parse.xname)
 fun add_const_attr (s1, s2) = Thm.declaration_attribute
   (fn th => Context.mapping (add_const_def s1 th s2) (fn x => x))
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (Attrib.setup (Binding.name "import_const") (Scan.lift parser >> add_const_attr)
-  "Declare a theorem as an equality that maps the given constant"))
+  "Declare a theorem as an equality that maps the given constant")
 
 val parser = Parse.name -- (Parse.name -- Parse.name)
 fun add_typ_attr (tyname, (absname, repname)) = Thm.declaration_attribute
   (fn th => Context.mapping (add_typ_def tyname absname repname th) (fn x => x))
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (Attrib.setup (Binding.name "import_type") (Scan.lift parser >> add_typ_attr)
-  "Declare a type_definion theorem as a map for an imported type abs rep"))
+  "Declare a type_definion theorem as a map for an imported type abs rep")
 
 val type_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
   (fn (ty_name1, ty_name2) => add_typ_map ty_name1 ty_name2)
@@ -115,11 +115,11 @@
 
 (* Initial type and constant maps, for types and constants that are not
    defined, which means their definitions do not appear in the proof dump *)
-val _ = Context.>> (Context.map_theory (
+val _ = Theory.setup
   add_typ_map "bool" @{type_name bool} o
   add_typ_map "fun" @{type_name fun} o
   add_typ_map "ind" @{type_name ind} o
   add_const_map "=" @{const_name HOL.eq} o
-  add_const_map "@" @{const_name "Eps"}))
+  add_const_map "@" @{const_name "Eps"})
 
 end
diff -r 96f7adb55d72 -r a5e54d4d9081 src/HOL/Tools/reflection.ML
--- a/src/HOL/Tools/reflection.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/HOL/Tools/reflection.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -65,11 +65,13 @@
 val add_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
 val del_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (Attrib.setup @{binding reify}
-    (Attrib.add_del add_reification_eq del_reification_eq) "declare reification equations" #>
-  Attrib.setup @{binding reflection}
-    (Attrib.add_del add_correctness_thm del_correctness_thm) "declare reflection correctness theorems"));
+    (Attrib.add_del add_reification_eq del_reification_eq)
+    "declare reification equations" #>
+   Attrib.setup @{binding reflection}
+    (Attrib.add_del add_correctness_thm del_correctness_thm)
+    "declare reflection correctness theorems");
 
 fun default_reify_tac ctxt user_eqs =
   let
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -385,7 +385,7 @@
 
 (* theory setup *)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
     "internal attribute" #>
   setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
@@ -427,7 +427,7 @@
   setup (Binding.name "abs_def")
     (Scan.succeed (Thm.rule_attribute (fn context =>
       Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
-    "abstract over free variables of definitional theorem"));
+    "abstract over free variables of definitional theorem");
 
 
 
@@ -506,7 +506,7 @@
 fun setup_config declare_config binding default =
   let
     val (config, setup) = declare_config binding default;
-    val _ = Context.>> (Context.map_theory setup);
+    val _ = Theory.setup setup;
   in config end;
 
 in
@@ -531,7 +531,7 @@
 fun setup_option coerce name =
   let
     val config = Config.declare_option name;
-    val _ = Context.>> (Context.map_theory (register_config config));
+    val _ = Theory.setup (register_config config);
   in coerce config end;
 
 in
@@ -551,7 +551,7 @@
 
 (* theory setup *)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (register_config quick_and_dirty_raw #>
   register_config Ast.trace_raw #>
   register_config Ast.stats_raw #>
@@ -582,6 +582,6 @@
   register_config Raw_Simplifier.simp_depth_limit_raw #>
   register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
   register_config Raw_Simplifier.simp_debug_raw #>
-  register_config Raw_Simplifier.simp_trace_raw));
+  register_config Raw_Simplifier.simp_trace_raw);
 
 end;
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/calculation.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -94,7 +94,7 @@
 
 (* concrete syntax *)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
     "declaration of transitivity rule" #>
   Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
@@ -103,7 +103,7 @@
     "resolution with symmetry rule" #>
   Global_Theory.add_thms
    [((Binding.empty, transitive_thm), [trans_add]),
-    ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
+    ((Binding.empty, symmetric_thm), [sym_add])] #> snd);
 
 
 
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/class.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -659,11 +659,11 @@
   HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
     default_intro_tac ctxt facts;
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
     "back-chain introduction rules of classes" #>
   Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
-    "apply some intro/elim rule"));
+    "apply some intro/elim rule");
 
 end;
 
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/code.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -320,9 +320,8 @@
         #> map_history_concluded (K true))
     |> SOME;
 
-val _ =
-  Context.>> (Context.map_theory
-    (Theory.at_begin continue_history #> Theory.at_end conclude_history));
+val _ = Theory.setup
+  (Theory.at_begin continue_history #> Theory.at_end conclude_history);
 
 
 (* access to data dependent on abstract executable code *)
@@ -1233,7 +1232,7 @@
 
 (* setup *)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
     val code_attribute_parser =
@@ -1247,7 +1246,7 @@
     Datatype_Interpretation.init
     #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
         "declare theorems for code generation"
-  end));
+  end);
 
 end; (*struct*)
 
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/context_rules.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -198,8 +198,8 @@
 val elim_query  = rule_add elim_queryK I;
 val dest_query  = rule_add elim_queryK Tactic.make_elim;
 
-val _ = Context.>> (Context.map_theory
-  (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]));
+val _ = Theory.setup
+  (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]);
 
 
 (* concrete syntax *)
@@ -208,7 +208,7 @@
   (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
     Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
     "declaration of introduction rule" #>
   Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
@@ -216,6 +216,6 @@
   Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
     "declaration of destruction rule" #>
   Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
-    "remove declaration of intro/elim/dest rule"));
+    "remove declaration of intro/elim/dest rule");
 
 end;
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -265,12 +265,11 @@
   Proof.goal (Toplevel.proof_of (diag_state ctxt))
     handle Toplevel.UNDEF => error "No goal present";
 
-val _ =
-  Context.>> (Context.map_theory
-   (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
-      (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
-    ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
-      (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
+val _ = Theory.setup
+  (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
+    (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
+   ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
+    (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
 
 
 (* print theorems *)
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -613,11 +613,11 @@
 val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
 val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
     "back-chain introduction rules of locales without unfolding predicates" #>
   Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
-    "back-chain all introduction rules of locales"));
+    "back-chain all introduction rules of locales");
 
 
 (*** diagnostic commands and interfaces ***)
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/method.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -438,7 +438,7 @@
 
 (* theory setup *)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
   setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
   setup (Binding.name "-") (Scan.succeed (K insert_facts))
@@ -470,7 +470,7 @@
   setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
     "ML tactic as proof method" #>
   setup (Binding.name "raw_tactic") (Scan.lift Args.name_source_position >> raw_tactic)
-    "ML tactic as raw proof method"));
+    "ML tactic as raw proof method");
 
 
 (*final declarations of this structure!*)
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/object_logic.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -174,7 +174,7 @@
 val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
 val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
 
-val _ = Context.>> (Context.map_theory (fold add_rulify Drule.norm_hhf_eqs));
+val _ = Theory.setup (fold add_rulify Drule.norm_hhf_eqs);
 
 
 (* atomize *)
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -163,12 +163,12 @@
 
 (* where: named instantiation *)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (Attrib.setup (Binding.name "where")
     (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
       (fn args =>
         Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
-    "named instantiation of theorem"));
+    "named instantiation of theorem");
 
 
 (* of: positional instantiation (terms only) *)
@@ -184,11 +184,11 @@
 
 in
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (Attrib.setup (Binding.name "of")
     (Scan.lift insts >> (fn args =>
       Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
-    "positional instantiation of theorem"));
+    "positional instantiation of theorem");
 
 end;
 
@@ -341,7 +341,7 @@
 
 (* setup *)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #>
   Method.setup (Binding.name "erule_tac") eres_inst_meth
     "apply rule in elimination manner (dynamic instantiation)" #>
@@ -358,7 +358,7 @@
   Method.setup (Binding.name "thin_tac")
     (Args.goal_spec -- Scan.lift Args.name_source >>
       (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
-      "remove premise (dynamic instantiation)"));
+      "remove premise (dynamic instantiation)");
 
 end;
 
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -54,8 +54,7 @@
 
 (** misc antiquotations **)
 
-val _ = Context.>> (Context.map_theory
-
+val _ = Theory.setup
  (inline (Binding.name "assert")
     (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
 
@@ -102,7 +101,7 @@
     (Args.context --
       Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
         "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
-          ML_Syntax.atomic (ML_Syntax.print_term t)))));
+          ML_Syntax.atomic (ML_Syntax.print_term t))));
 
 
 (* type classes *)
@@ -112,13 +111,13 @@
   |> syn ? Lexicon.mark_class
   |> ML_Syntax.print_string);
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (inline (Binding.name "class") (class false) #>
   inline (Binding.name "class_syntax") (class true) #>
 
   inline (Binding.name "sort")
     (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
-      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))));
+      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
 
 
 (* type constructors *)
@@ -134,7 +133,7 @@
         | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
     in ML_Syntax.print_string res end);
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (inline (Binding.name "type_name")
     (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
   inline (Binding.name "type_abbrev")
@@ -142,7 +141,7 @@
   inline (Binding.name "nonterminal")
     (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
   inline (Binding.name "type_syntax")
-    (type_name "type" (fn (c, _) => Lexicon.mark_type c))));
+    (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
 
 
 (* constants *)
@@ -155,7 +154,7 @@
         handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
     in ML_Syntax.print_string res end);
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (inline (Binding.name "const_name")
     (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
   inline (Binding.name "const_abbrev")
@@ -181,7 +180,7 @@
             error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
               quote c ^ enclose "(" ")" (commas (replicate n "_")));
           val const = Const (c, Consts.instance consts (c, Ts));
-        in ML_Syntax.atomic (ML_Syntax.print_term const) end))));
+        in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
 
 
 (* outer syntax *)
@@ -191,7 +190,7 @@
     (f ((name, Thy_Header.the_keyword thy name), pos)
       handle ERROR msg => error (msg ^ Position.here pos)));
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (value (Binding.name "keyword")
     (with_keyword
       (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
@@ -209,7 +208,7 @@
                   (ML_Syntax.print_list ML_Syntax.print_string)))
               ML_Syntax.print_position) ((name, kind), pos))
         | ((name, NONE), pos) =>
-            error ("Expected command keyword " ^ quote name ^ Position.here pos)))));
+            error ("Expected command keyword " ^ quote name ^ Position.here pos))));
 
 end;
 
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -74,7 +74,7 @@
   let
     val ths' = Context.>>> (Context.map_theory_result
       (Global_Theory.store_thms (Binding.name name, ths)));
-    val _ = Context.>> (Context.map_theory (Stored_Thms.put ths'));
+    val _ = Theory.setup (Stored_Thms.put ths');
     val _ =
       if name = "" then ()
       else if not (ML_Syntax.is_identifier name) then
@@ -82,7 +82,7 @@
       else
         ML_Compiler.eval true Position.none
           (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
-    val _ = Context.>> (Context.map_theory (Stored_Thms.put []));
+    val _ = Theory.setup (Stored_Thms.put []);
   in () end;
 
 val ml_store_thms = ml_store "ML_Context.get_stored_thms";
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/ML/ml_thms.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -34,23 +34,22 @@
 
 (* attribute source *)
 
-val _ =
-  Context.>> (Context.map_theory
-    (ML_Context.add_antiq (Binding.name "attributes")
-      (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
-        let
-          val ctxt = Context.the_proof context;
-          val thy = Proof_Context.theory_of ctxt;
+val _ = Theory.setup
+  (ML_Context.add_antiq (Binding.name "attributes")
+    (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
+      let
+        val ctxt = Context.the_proof context;
+        val thy = Proof_Context.theory_of ctxt;
 
-          val i = serial ();
-          val srcs = map (Attrib.intern_src thy) raw_srcs;
-          val _ = map (Attrib.attribute ctxt) srcs;
-          val (a, ctxt') = ctxt
-            |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
-          val ml =
-            ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
-              string_of_int i ^ ";\n", "Isabelle." ^ a);
-        in (Context.Proof ctxt', K ml) end)))));
+        val i = serial ();
+        val srcs = map (Attrib.intern_src thy) raw_srcs;
+        val _ = map (Attrib.attribute ctxt) srcs;
+        val (a, ctxt') = ctxt
+          |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
+        val ml =
+          ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
+            string_of_int i ^ ";\n", "Isabelle." ^ a);
+      in (Context.Proof ctxt', K ml) end))));
 
 
 (* fact references *)
@@ -73,14 +72,13 @@
       else ("", ml_body);
   in (Context.Proof ctxt'', decl) end;
 
-val _ =
-  Context.>> (Context.map_theory
-    (ML_Context.add_antiq (Binding.name "thm")
-      (Scan.depend (fn context =>
-        Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
-     ML_Context.add_antiq (Binding.name "thms")
-      (Scan.depend (fn context =>
-        Scan.pass context Attrib.thms >> thm_binding "thms" false context))));
+val _ = Theory.setup
+  (ML_Context.add_antiq (Binding.name "thm")
+    (Scan.depend (fn context =>
+      Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
+   ML_Context.add_antiq (Binding.name "thms")
+    (Scan.depend (fn context =>
+      Scan.pass context Attrib.thms >> thm_binding "thms" false context)));
 
 
 (* ad-hoc goals *)
@@ -89,9 +87,8 @@
 val by = Args.$$$ "by";
 val goal = Scan.unless (by || and_) Args.name_source;
 
-val _ =
-  Context.>> (Context.map_theory
-   (ML_Context.add_antiq (Binding.name "lemma")
+val _ = Theory.setup
+  (ML_Context.add_antiq (Binding.name "lemma")
     (Scan.depend (fn context =>
       Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) --
       (by |-- Method.parse -- Scan.option Method.parse) >>
@@ -111,7 +108,7 @@
             val thms =
               Proof_Context.get_fact ctxt'
                 (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
-          in thm_binding "lemma" (length (flat propss) = 1) context thms end)))));
+          in thm_binding "lemma" (length (flat propss) = 1) context thms end))));
 
 end;
 
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -422,7 +422,7 @@
 
 (** Pure setup **)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (add_types [("prop", ([], NONE))] #>
 
    add_typeof_eqns
@@ -469,7 +469,7 @@
    Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
      "specify theorems to be expanded during extraction" #>
    Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
-     "specify definitions to be expanded during extraction"));
+     "specify definitions to be expanded during extraction");
 
 
 (**** extract program ****)
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -190,7 +190,7 @@
   in rew' #> Option.map (rpair Proofterm.no_skel) end;
 
 fun rprocs b = [rew b];
-val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));
+val _ = Theory.setup (fold Proofterm.add_prf_rproc (rprocs false));
 
 
 (**** apply rewriting function to all terms in proof ****)
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -807,14 +807,14 @@
 
 (* setup translations *)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (Sign.parse_ast_translation
    [("_context_const", const_ast_tr true),
     ("_context_xconst", const_ast_tr false)] #>
   Sign.typed_print_translation
    [("_type_prop", type_prop_tr'),
     ("\\<^const>TYPE", type_tr'),
-    ("_type_constraint_", type_constraint_tr')]));
+    ("_type_constraint_", type_constraint_tr')]);
 
 
 
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Thy/present.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -52,8 +52,8 @@
   fun merge _ = empty;
 );
 
-val _ = Context.>> (Context.map_theory
-  (Browser_Info.put {chapter = Context.PureN, name = Context.PureN}));
+val _ = Theory.setup
+  (Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
 
 val session_name = #name o Browser_Info.get;
 val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Thy/rail.ML
--- a/src/Pure/Thy/rail.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Thy/rail.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -263,11 +263,10 @@
 
 in
 
-val _ =
-  Context.>> (Context.map_theory
-    (Thy_Output.antiquotation (Binding.name "rail")
-      (Scan.lift (Parse.source_position Parse.string))
-      (fn {state, ...} => output_rules state o read)));
+val _ = Theory.setup
+  (Thy_Output.antiquotation (Binding.name "rail")
+    (Scan.lift (Parse.source_position Parse.string))
+    (fn {state, ...} => output_rules state o read));
 
 end;
 
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Thy/term_style.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -91,11 +91,11 @@
   | sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b)
   | sub_term t = t;
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (setup "lhs" (style_lhs_rhs fst) #>
   setup "rhs" (style_lhs_rhs snd) #>
   setup "prem" style_prem #>
   setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
-  setup "sub" (Scan.succeed (K sub_term))));
+  setup "sub" (Scan.succeed (K sub_term)));
 
 end;
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Thy/thy_load.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -275,9 +275,8 @@
 
 (* document antiquotation *)
 
-val _ =
-  Context.>> (Context.map_theory
-   (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
+val _ = Theory.setup
+  (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
     (fn {context = ctxt, ...} => fn (name, pos) =>
       let
         val dir = master_directory (Proof_Context.theory_of ctxt);
@@ -290,7 +289,7 @@
         space_explode "/" name
         |> map Thy_Output.verb_text
         |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
-      end)));
+      end));
 
 
 (* global master path *)
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -442,25 +442,24 @@
 
 (* options *)
 
-val _ =
-  Context.>> (Context.map_theory
-   (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
-    add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
-    add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
-    add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
-    add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
-    add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
-    add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
-    add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
-    add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
-    add_option (Binding.name "display") (Config.put display o boolean) #>
-    add_option (Binding.name "break") (Config.put break o boolean) #>
-    add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
-    add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
-    add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
-    add_option (Binding.name "indent") (Config.put indent o integer) #>
-    add_option (Binding.name "source") (Config.put source o boolean) #>
-    add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer)));
+val _ = Theory.setup
+ (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
+  add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
+  add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
+  add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
+  add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
+  add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
+  add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
+  add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
+  add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
+  add_option (Binding.name "display") (Config.put display o boolean) #>
+  add_option (Binding.name "break") (Config.put break o boolean) #>
+  add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
+  add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
+  add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
+  add_option (Binding.name "indent") (Config.put indent o integer) #>
+  add_option (Binding.name "source") (Config.put source o boolean) #>
+  add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer));
 
 
 (* basic pretty printing *)
@@ -564,22 +563,21 @@
 
 in
 
-val _ =
-  Context.>> (Context.map_theory
-   (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
-    basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
-    basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
-    basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
-    basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
-    basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
-    basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
-    basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
-    basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
-    basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
-    basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
-    basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
-    basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
-    basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory));
+val _ = Theory.setup
+ (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
+  basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
+  basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
+  basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
+  basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
+  basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
+  basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
+  basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
+  basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
+  basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
+  basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
+  basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
+  basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
+  basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);
 
 end;
 
@@ -600,10 +598,9 @@
 
 in
 
-val _ =
-  Context.>> (Context.map_theory
-   (goal_state (Binding.name "goals") true #>
-    goal_state (Binding.name "subgoals") false));
+val _ = Theory.setup
+ (goal_state (Binding.name "goals") true #>
+  goal_state (Binding.name "subgoals") false);
 
 end;
 
@@ -612,9 +609,8 @@
 
 val _ = Keyword.define ("by", NONE);  (*overlap with command category*)
 
-val _ =
-  Context.>> (Context.map_theory
-   (antiquotation (Binding.name "lemma")
+val _ = Theory.setup
+  (antiquotation (Binding.name "lemma")
     (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
     (fn {source, context, ...} => fn (prop, methods) =>
       let
@@ -624,7 +620,7 @@
         val _ = context
           |> Proof.theorem NONE (K I) [[(prop, [])]]
           |> Proof.global_terminal_proof methods;
-      in output context (maybe_pretty_source pretty_term context prop_src [prop]) end)));
+      in output context (maybe_pretty_source pretty_term context prop_src [prop]) end));
 
 
 (* ML text *)
@@ -649,20 +645,19 @@
 
 in
 
-val _ =
-  Context.>> (Context.map_theory
-   (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
-    ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
-    ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
-    ml_text (Binding.name "ML_struct")
-      (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
+val _ = Theory.setup
+ (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
+  ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
+  ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
+  ml_text (Binding.name "ML_struct")
+    (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
 
-    ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
-      (fn pos => fn txt =>
-        ML_Lex.read Position.none ("ML_Env.check_functor " ^
-          ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
+  ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
+    (fn pos => fn txt =>
+      ML_Lex.read Position.none ("ML_Env.check_functor " ^
+        ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
 
-    ml_text (Binding.name "ML_text") (K (K []))));
+  ml_text (Binding.name "ML_text") (K (K [])));
 
 end;
 
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/axclass.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -264,9 +264,8 @@
     else SOME (map_proven_arities (K arities') thy)
   end;
 
-val _ = Context.>> (Context.map_theory
-  (Theory.at_begin complete_classrels #>
-   Theory.at_begin complete_arities));
+val _ = Theory.setup
+  (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities);
 
 val _ = Proofterm.install_axclass_proofs
   {classrel_proof = Thm.proof_of oo the_classrel,
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/pure_thy.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -56,7 +56,7 @@
 val token_markers =
   ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
    Old_Appl_Syntax.put false #>
    Sign.add_types_global
@@ -221,6 +221,6 @@
   #> Sign.hide_const false "Pure.conjunction"
   #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
   #> fold (fn (a, prop) =>
-      snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms));
+      snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms);
 
 end;
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/simplifier.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -129,10 +129,10 @@
 (* global simprocs *)
 
 fun Addsimprocs args =
-  Context.>> (Context.map_theory (map_theory_simpset (fn ctxt => ctxt addsimprocs args)));
+  Theory.setup (map_theory_simpset (fn ctxt => ctxt addsimprocs args));
 
 fun Delsimprocs args =
-  Context.>> (Context.map_theory (map_theory_simpset (fn ctxt => ctxt delsimprocs args)));
+  Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs args));
 
 
 
@@ -154,13 +154,11 @@
 fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
 val the_simproc = Name_Space.get o get_simprocs;
 
-val _ =
-  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 " ^
-            ML_Syntax.print_string (check_simproc ctxt name)))));
+val _ = Theory.setup
+  (ML_Antiquote.value (Binding.name "simproc")
+    (Args.context -- Scan.lift (Parse.position Args.name)
+      >> (fn (ctxt, name) =>
+        "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
 
 
 (* define simprocs *)
@@ -327,14 +325,14 @@
 
 (* setup attributes *)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
  (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
     "declaration of Simplifier rewrite rule" #>
   Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
     "declaration of Simplifier congruence rule" #>
   Attrib.setup (Binding.name "simproc") simproc_att
     "declaration of simplification procedures" #>
-  Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
+  Attrib.setup (Binding.name "simplified") simplified "simplified rule");
 
 
 
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/theory.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -15,6 +15,7 @@
   val merge: theory * theory -> theory
   val merge_list: theory list -> theory
   val requires: theory -> string -> string -> unit
+  val setup: (theory -> theory) -> unit
   val get_markup: theory -> Markup.T
   val axiom_space: theory -> Name_Space.T
   val axiom_table: theory -> term Symtab.table
@@ -59,6 +60,8 @@
   if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then ()
   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
 
+fun setup f = Context.>> (Context.map_theory f);
+
 
 
 (** datatype thy **)
diff -r 96f7adb55d72 -r a5e54d4d9081 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.";
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Tools/Spec_Check/output_style.ML
--- a/src/Tools/Spec_Check/output_style.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Tools/Spec_Check/output_style.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -78,6 +78,8 @@
         {status = status, finish = finish}
       end)
 
+val _ = Theory.setup perl_style;
+
 
 (* CM style: meshes with CM output; highlighted in sml-mode *)
 
@@ -106,9 +108,6 @@
         {status = K (), finish = finish}
       end)
 
-
-(* setup *)
-
-val _ = Context.>> (Context.map_theory (perl_style #> cm_style));
+val _ = Theory.setup cm_style;
 
 end
diff -r 96f7adb55d72 -r a5e54d4d9081 src/Tools/try.ML
--- a/src/Tools/try.ML	Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Tools/try.ML	Fri Aug 23 20:35:50 2013 +0200
@@ -142,7 +142,6 @@
 
 (* hybrid tool setup *)
 
-fun tool_setup tool =
-  (Context.>> (Context.map_theory (register_tool tool)); print_function tool)
+fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool)
 
 end;