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;