src/Pure/Isar/attrib.ML
changeset 53171 a5e54d4d9081
parent 53168 d998de7f0efc
child 55140 7eb0c04e4c40
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Aug 23 20:09:34 2013 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Aug 23 20:35:50 2013 +0200
     1.3 @@ -385,7 +385,7 @@
     1.4  
     1.5  (* theory setup *)
     1.6  
     1.7 -val _ = Context.>> (Context.map_theory
     1.8 +val _ = Theory.setup
     1.9   (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
    1.10      "internal attribute" #>
    1.11    setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
    1.12 @@ -427,7 +427,7 @@
    1.13    setup (Binding.name "abs_def")
    1.14      (Scan.succeed (Thm.rule_attribute (fn context =>
    1.15        Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
    1.16 -    "abstract over free variables of definitional theorem"));
    1.17 +    "abstract over free variables of definitional theorem");
    1.18  
    1.19  
    1.20  
    1.21 @@ -506,7 +506,7 @@
    1.22  fun setup_config declare_config binding default =
    1.23    let
    1.24      val (config, setup) = declare_config binding default;
    1.25 -    val _ = Context.>> (Context.map_theory setup);
    1.26 +    val _ = Theory.setup setup;
    1.27    in config end;
    1.28  
    1.29  in
    1.30 @@ -531,7 +531,7 @@
    1.31  fun setup_option coerce name =
    1.32    let
    1.33      val config = Config.declare_option name;
    1.34 -    val _ = Context.>> (Context.map_theory (register_config config));
    1.35 +    val _ = Theory.setup (register_config config);
    1.36    in coerce config end;
    1.37  
    1.38  in
    1.39 @@ -551,7 +551,7 @@
    1.40  
    1.41  (* theory setup *)
    1.42  
    1.43 -val _ = Context.>> (Context.map_theory
    1.44 +val _ = Theory.setup
    1.45   (register_config quick_and_dirty_raw #>
    1.46    register_config Ast.trace_raw #>
    1.47    register_config Ast.stats_raw #>
    1.48 @@ -582,6 +582,6 @@
    1.49    register_config Raw_Simplifier.simp_depth_limit_raw #>
    1.50    register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
    1.51    register_config Raw_Simplifier.simp_debug_raw #>
    1.52 -  register_config Raw_Simplifier.simp_trace_raw));
    1.53 +  register_config Raw_Simplifier.simp_trace_raw);
    1.54  
    1.55  end;