--- 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;