added Theory.setup convenience;
authorwenzelm
Fri Aug 23 20:35:50 2013 +0200 (2013-08-23 ago)
changeset 53171a5e54d4d9081
parent 53170 96f7adb55d72
child 53172 31e24d6ff1ea
added Theory.setup convenience;
src/HOL/Import/import_data.ML
src/HOL/Tools/reflection.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/rule_insts.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_thms.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/present.ML
src/Pure/Thy/rail.ML
src/Pure/Thy/term_style.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_output.ML
src/Pure/axclass.ML
src/Pure/pure_thy.ML
src/Pure/simplifier.ML
src/Pure/theory.ML
src/Tools/Code/code_runtime.ML
src/Tools/Spec_Check/output_style.ML
src/Tools/try.ML
     1.1 --- a/src/HOL/Import/import_data.ML	Fri Aug 23 20:09:34 2013 +0200
     1.2 +++ b/src/HOL/Import/import_data.ML	Fri Aug 23 20:35:50 2013 +0200
     1.3 @@ -90,16 +90,16 @@
     1.4  val parser = Parse.name -- Scan.option (Parse.$$$ ":" |-- Parse.xname)
     1.5  fun add_const_attr (s1, s2) = Thm.declaration_attribute
     1.6    (fn th => Context.mapping (add_const_def s1 th s2) (fn x => x))
     1.7 -val _ = Context.>> (Context.map_theory
     1.8 +val _ = Theory.setup
     1.9    (Attrib.setup (Binding.name "import_const") (Scan.lift parser >> add_const_attr)
    1.10 -  "Declare a theorem as an equality that maps the given constant"))
    1.11 +  "Declare a theorem as an equality that maps the given constant")
    1.12  
    1.13  val parser = Parse.name -- (Parse.name -- Parse.name)
    1.14  fun add_typ_attr (tyname, (absname, repname)) = Thm.declaration_attribute
    1.15    (fn th => Context.mapping (add_typ_def tyname absname repname th) (fn x => x))
    1.16 -val _ = Context.>> (Context.map_theory
    1.17 +val _ = Theory.setup
    1.18    (Attrib.setup (Binding.name "import_type") (Scan.lift parser >> add_typ_attr)
    1.19 -  "Declare a type_definion theorem as a map for an imported type abs rep"))
    1.20 +  "Declare a type_definion theorem as a map for an imported type abs rep")
    1.21  
    1.22  val type_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
    1.23    (fn (ty_name1, ty_name2) => add_typ_map ty_name1 ty_name2)
    1.24 @@ -115,11 +115,11 @@
    1.25  
    1.26  (* Initial type and constant maps, for types and constants that are not
    1.27     defined, which means their definitions do not appear in the proof dump *)
    1.28 -val _ = Context.>> (Context.map_theory (
    1.29 +val _ = Theory.setup
    1.30    add_typ_map "bool" @{type_name bool} o
    1.31    add_typ_map "fun" @{type_name fun} o
    1.32    add_typ_map "ind" @{type_name ind} o
    1.33    add_const_map "=" @{const_name HOL.eq} o
    1.34 -  add_const_map "@" @{const_name "Eps"}))
    1.35 +  add_const_map "@" @{const_name "Eps"})
    1.36  
    1.37  end
     2.1 --- a/src/HOL/Tools/reflection.ML	Fri Aug 23 20:09:34 2013 +0200
     2.2 +++ b/src/HOL/Tools/reflection.ML	Fri Aug 23 20:35:50 2013 +0200
     2.3 @@ -65,11 +65,13 @@
     2.4  val add_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
     2.5  val del_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
     2.6  
     2.7 -val _ = Context.>> (Context.map_theory
     2.8 +val _ = Theory.setup
     2.9    (Attrib.setup @{binding reify}
    2.10 -    (Attrib.add_del add_reification_eq del_reification_eq) "declare reification equations" #>
    2.11 -  Attrib.setup @{binding reflection}
    2.12 -    (Attrib.add_del add_correctness_thm del_correctness_thm) "declare reflection correctness theorems"));
    2.13 +    (Attrib.add_del add_reification_eq del_reification_eq)
    2.14 +    "declare reification equations" #>
    2.15 +   Attrib.setup @{binding reflection}
    2.16 +    (Attrib.add_del add_correctness_thm del_correctness_thm)
    2.17 +    "declare reflection correctness theorems");
    2.18  
    2.19  fun default_reify_tac ctxt user_eqs =
    2.20    let
     3.1 --- a/src/Pure/Isar/attrib.ML	Fri Aug 23 20:09:34 2013 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Fri Aug 23 20:35:50 2013 +0200
     3.3 @@ -385,7 +385,7 @@
     3.4  
     3.5  (* theory setup *)
     3.6  
     3.7 -val _ = Context.>> (Context.map_theory
     3.8 +val _ = Theory.setup
     3.9   (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
    3.10      "internal attribute" #>
    3.11    setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
    3.12 @@ -427,7 +427,7 @@
    3.13    setup (Binding.name "abs_def")
    3.14      (Scan.succeed (Thm.rule_attribute (fn context =>
    3.15        Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
    3.16 -    "abstract over free variables of definitional theorem"));
    3.17 +    "abstract over free variables of definitional theorem");
    3.18  
    3.19  
    3.20  
    3.21 @@ -506,7 +506,7 @@
    3.22  fun setup_config declare_config binding default =
    3.23    let
    3.24      val (config, setup) = declare_config binding default;
    3.25 -    val _ = Context.>> (Context.map_theory setup);
    3.26 +    val _ = Theory.setup setup;
    3.27    in config end;
    3.28  
    3.29  in
    3.30 @@ -531,7 +531,7 @@
    3.31  fun setup_option coerce name =
    3.32    let
    3.33      val config = Config.declare_option name;
    3.34 -    val _ = Context.>> (Context.map_theory (register_config config));
    3.35 +    val _ = Theory.setup (register_config config);
    3.36    in coerce config end;
    3.37  
    3.38  in
    3.39 @@ -551,7 +551,7 @@
    3.40  
    3.41  (* theory setup *)
    3.42  
    3.43 -val _ = Context.>> (Context.map_theory
    3.44 +val _ = Theory.setup
    3.45   (register_config quick_and_dirty_raw #>
    3.46    register_config Ast.trace_raw #>
    3.47    register_config Ast.stats_raw #>
    3.48 @@ -582,6 +582,6 @@
    3.49    register_config Raw_Simplifier.simp_depth_limit_raw #>
    3.50    register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
    3.51    register_config Raw_Simplifier.simp_debug_raw #>
    3.52 -  register_config Raw_Simplifier.simp_trace_raw));
    3.53 +  register_config Raw_Simplifier.simp_trace_raw);
    3.54  
    3.55  end;
     4.1 --- a/src/Pure/Isar/calculation.ML	Fri Aug 23 20:09:34 2013 +0200
     4.2 +++ b/src/Pure/Isar/calculation.ML	Fri Aug 23 20:35:50 2013 +0200
     4.3 @@ -94,7 +94,7 @@
     4.4  
     4.5  (* concrete syntax *)
     4.6  
     4.7 -val _ = Context.>> (Context.map_theory
     4.8 +val _ = Theory.setup
     4.9   (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
    4.10      "declaration of transitivity rule" #>
    4.11    Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
    4.12 @@ -103,7 +103,7 @@
    4.13      "resolution with symmetry rule" #>
    4.14    Global_Theory.add_thms
    4.15     [((Binding.empty, transitive_thm), [trans_add]),
    4.16 -    ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
    4.17 +    ((Binding.empty, symmetric_thm), [sym_add])] #> snd);
    4.18  
    4.19  
    4.20  
     5.1 --- a/src/Pure/Isar/class.ML	Fri Aug 23 20:09:34 2013 +0200
     5.2 +++ b/src/Pure/Isar/class.ML	Fri Aug 23 20:35:50 2013 +0200
     5.3 @@ -659,11 +659,11 @@
     5.4    HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
     5.5      default_intro_tac ctxt facts;
     5.6  
     5.7 -val _ = Context.>> (Context.map_theory
     5.8 +val _ = Theory.setup
     5.9   (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
    5.10      "back-chain introduction rules of classes" #>
    5.11    Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
    5.12 -    "apply some intro/elim rule"));
    5.13 +    "apply some intro/elim rule");
    5.14  
    5.15  end;
    5.16  
     6.1 --- a/src/Pure/Isar/code.ML	Fri Aug 23 20:09:34 2013 +0200
     6.2 +++ b/src/Pure/Isar/code.ML	Fri Aug 23 20:35:50 2013 +0200
     6.3 @@ -320,9 +320,8 @@
     6.4          #> map_history_concluded (K true))
     6.5      |> SOME;
     6.6  
     6.7 -val _ =
     6.8 -  Context.>> (Context.map_theory
     6.9 -    (Theory.at_begin continue_history #> Theory.at_end conclude_history));
    6.10 +val _ = Theory.setup
    6.11 +  (Theory.at_begin continue_history #> Theory.at_end conclude_history);
    6.12  
    6.13  
    6.14  (* access to data dependent on abstract executable code *)
    6.15 @@ -1233,7 +1232,7 @@
    6.16  
    6.17  (* setup *)
    6.18  
    6.19 -val _ = Context.>> (Context.map_theory
    6.20 +val _ = Theory.setup
    6.21    (let
    6.22      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    6.23      val code_attribute_parser =
    6.24 @@ -1247,7 +1246,7 @@
    6.25      Datatype_Interpretation.init
    6.26      #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
    6.27          "declare theorems for code generation"
    6.28 -  end));
    6.29 +  end);
    6.30  
    6.31  end; (*struct*)
    6.32  
     7.1 --- a/src/Pure/Isar/context_rules.ML	Fri Aug 23 20:09:34 2013 +0200
     7.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Aug 23 20:35:50 2013 +0200
     7.3 @@ -198,8 +198,8 @@
     7.4  val elim_query  = rule_add elim_queryK I;
     7.5  val dest_query  = rule_add elim_queryK Tactic.make_elim;
     7.6  
     7.7 -val _ = Context.>> (Context.map_theory
     7.8 -  (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]));
     7.9 +val _ = Theory.setup
    7.10 +  (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]);
    7.11  
    7.12  
    7.13  (* concrete syntax *)
    7.14 @@ -208,7 +208,7 @@
    7.15    (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
    7.16      Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
    7.17  
    7.18 -val _ = Context.>> (Context.map_theory
    7.19 +val _ = Theory.setup
    7.20   (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
    7.21      "declaration of introduction rule" #>
    7.22    Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
    7.23 @@ -216,6 +216,6 @@
    7.24    Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
    7.25      "declaration of destruction rule" #>
    7.26    Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
    7.27 -    "remove declaration of intro/elim/dest rule"));
    7.28 +    "remove declaration of intro/elim/dest rule");
    7.29  
    7.30  end;
     8.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 20:09:34 2013 +0200
     8.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 20:35:50 2013 +0200
     8.3 @@ -265,12 +265,11 @@
     8.4    Proof.goal (Toplevel.proof_of (diag_state ctxt))
     8.5      handle Toplevel.UNDEF => error "No goal present";
     8.6  
     8.7 -val _ =
     8.8 -  Context.>> (Context.map_theory
     8.9 -   (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
    8.10 -      (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
    8.11 -    ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
    8.12 -      (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
    8.13 +val _ = Theory.setup
    8.14 +  (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
    8.15 +    (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
    8.16 +   ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
    8.17 +    (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
    8.18  
    8.19  
    8.20  (* print theorems *)
     9.1 --- a/src/Pure/Isar/locale.ML	Fri Aug 23 20:09:34 2013 +0200
     9.2 +++ b/src/Pure/Isar/locale.ML	Fri Aug 23 20:35:50 2013 +0200
     9.3 @@ -613,11 +613,11 @@
     9.4  val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
     9.5  val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
     9.6  
     9.7 -val _ = Context.>> (Context.map_theory
     9.8 +val _ = Theory.setup
     9.9   (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
    9.10      "back-chain introduction rules of locales without unfolding predicates" #>
    9.11    Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
    9.12 -    "back-chain all introduction rules of locales"));
    9.13 +    "back-chain all introduction rules of locales");
    9.14  
    9.15  
    9.16  (*** diagnostic commands and interfaces ***)
    10.1 --- a/src/Pure/Isar/method.ML	Fri Aug 23 20:09:34 2013 +0200
    10.2 +++ b/src/Pure/Isar/method.ML	Fri Aug 23 20:35:50 2013 +0200
    10.3 @@ -438,7 +438,7 @@
    10.4  
    10.5  (* theory setup *)
    10.6  
    10.7 -val _ = Context.>> (Context.map_theory
    10.8 +val _ = Theory.setup
    10.9   (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
   10.10    setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
   10.11    setup (Binding.name "-") (Scan.succeed (K insert_facts))
   10.12 @@ -470,7 +470,7 @@
   10.13    setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
   10.14      "ML tactic as proof method" #>
   10.15    setup (Binding.name "raw_tactic") (Scan.lift Args.name_source_position >> raw_tactic)
   10.16 -    "ML tactic as raw proof method"));
   10.17 +    "ML tactic as raw proof method");
   10.18  
   10.19  
   10.20  (*final declarations of this structure!*)
    11.1 --- a/src/Pure/Isar/object_logic.ML	Fri Aug 23 20:09:34 2013 +0200
    11.2 +++ b/src/Pure/Isar/object_logic.ML	Fri Aug 23 20:35:50 2013 +0200
    11.3 @@ -174,7 +174,7 @@
    11.4  val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
    11.5  val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
    11.6  
    11.7 -val _ = Context.>> (Context.map_theory (fold add_rulify Drule.norm_hhf_eqs));
    11.8 +val _ = Theory.setup (fold add_rulify Drule.norm_hhf_eqs);
    11.9  
   11.10  
   11.11  (* atomize *)
    12.1 --- a/src/Pure/Isar/rule_insts.ML	Fri Aug 23 20:09:34 2013 +0200
    12.2 +++ b/src/Pure/Isar/rule_insts.ML	Fri Aug 23 20:35:50 2013 +0200
    12.3 @@ -163,12 +163,12 @@
    12.4  
    12.5  (* where: named instantiation *)
    12.6  
    12.7 -val _ = Context.>> (Context.map_theory
    12.8 +val _ = Theory.setup
    12.9    (Attrib.setup (Binding.name "where")
   12.10      (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
   12.11        (fn args =>
   12.12          Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
   12.13 -    "named instantiation of theorem"));
   12.14 +    "named instantiation of theorem");
   12.15  
   12.16  
   12.17  (* of: positional instantiation (terms only) *)
   12.18 @@ -184,11 +184,11 @@
   12.19  
   12.20  in
   12.21  
   12.22 -val _ = Context.>> (Context.map_theory
   12.23 +val _ = Theory.setup
   12.24    (Attrib.setup (Binding.name "of")
   12.25      (Scan.lift insts >> (fn args =>
   12.26        Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
   12.27 -    "positional instantiation of theorem"));
   12.28 +    "positional instantiation of theorem");
   12.29  
   12.30  end;
   12.31  
   12.32 @@ -341,7 +341,7 @@
   12.33  
   12.34  (* setup *)
   12.35  
   12.36 -val _ = Context.>> (Context.map_theory
   12.37 +val _ = Theory.setup
   12.38   (Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #>
   12.39    Method.setup (Binding.name "erule_tac") eres_inst_meth
   12.40      "apply rule in elimination manner (dynamic instantiation)" #>
   12.41 @@ -358,7 +358,7 @@
   12.42    Method.setup (Binding.name "thin_tac")
   12.43      (Args.goal_spec -- Scan.lift Args.name_source >>
   12.44        (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
   12.45 -      "remove premise (dynamic instantiation)"));
   12.46 +      "remove premise (dynamic instantiation)");
   12.47  
   12.48  end;
   12.49  
    13.1 --- a/src/Pure/ML/ml_antiquote.ML	Fri Aug 23 20:09:34 2013 +0200
    13.2 +++ b/src/Pure/ML/ml_antiquote.ML	Fri Aug 23 20:35:50 2013 +0200
    13.3 @@ -54,8 +54,7 @@
    13.4  
    13.5  (** misc antiquotations **)
    13.6  
    13.7 -val _ = Context.>> (Context.map_theory
    13.8 -
    13.9 +val _ = Theory.setup
   13.10   (inline (Binding.name "assert")
   13.11      (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
   13.12  
   13.13 @@ -102,7 +101,7 @@
   13.14      (Args.context --
   13.15        Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
   13.16          "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   13.17 -          ML_Syntax.atomic (ML_Syntax.print_term t)))));
   13.18 +          ML_Syntax.atomic (ML_Syntax.print_term t))));
   13.19  
   13.20  
   13.21  (* type classes *)
   13.22 @@ -112,13 +111,13 @@
   13.23    |> syn ? Lexicon.mark_class
   13.24    |> ML_Syntax.print_string);
   13.25  
   13.26 -val _ = Context.>> (Context.map_theory
   13.27 +val _ = Theory.setup
   13.28   (inline (Binding.name "class") (class false) #>
   13.29    inline (Binding.name "class_syntax") (class true) #>
   13.30  
   13.31    inline (Binding.name "sort")
   13.32      (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
   13.33 -      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))));
   13.34 +      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
   13.35  
   13.36  
   13.37  (* type constructors *)
   13.38 @@ -134,7 +133,7 @@
   13.39          | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
   13.40      in ML_Syntax.print_string res end);
   13.41  
   13.42 -val _ = Context.>> (Context.map_theory
   13.43 +val _ = Theory.setup
   13.44   (inline (Binding.name "type_name")
   13.45      (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
   13.46    inline (Binding.name "type_abbrev")
   13.47 @@ -142,7 +141,7 @@
   13.48    inline (Binding.name "nonterminal")
   13.49      (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
   13.50    inline (Binding.name "type_syntax")
   13.51 -    (type_name "type" (fn (c, _) => Lexicon.mark_type c))));
   13.52 +    (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
   13.53  
   13.54  
   13.55  (* constants *)
   13.56 @@ -155,7 +154,7 @@
   13.57          handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   13.58      in ML_Syntax.print_string res end);
   13.59  
   13.60 -val _ = Context.>> (Context.map_theory
   13.61 +val _ = Theory.setup
   13.62   (inline (Binding.name "const_name")
   13.63      (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
   13.64    inline (Binding.name "const_abbrev")
   13.65 @@ -181,7 +180,7 @@
   13.66              error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
   13.67                quote c ^ enclose "(" ")" (commas (replicate n "_")));
   13.68            val const = Const (c, Consts.instance consts (c, Ts));
   13.69 -        in ML_Syntax.atomic (ML_Syntax.print_term const) end))));
   13.70 +        in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
   13.71  
   13.72  
   13.73  (* outer syntax *)
   13.74 @@ -191,7 +190,7 @@
   13.75      (f ((name, Thy_Header.the_keyword thy name), pos)
   13.76        handle ERROR msg => error (msg ^ Position.here pos)));
   13.77  
   13.78 -val _ = Context.>> (Context.map_theory
   13.79 +val _ = Theory.setup
   13.80   (value (Binding.name "keyword")
   13.81      (with_keyword
   13.82        (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
   13.83 @@ -209,7 +208,7 @@
   13.84                    (ML_Syntax.print_list ML_Syntax.print_string)))
   13.85                ML_Syntax.print_position) ((name, kind), pos))
   13.86          | ((name, NONE), pos) =>
   13.87 -            error ("Expected command keyword " ^ quote name ^ Position.here pos)))));
   13.88 +            error ("Expected command keyword " ^ quote name ^ Position.here pos))));
   13.89  
   13.90  end;
   13.91  
    14.1 --- a/src/Pure/ML/ml_context.ML	Fri Aug 23 20:09:34 2013 +0200
    14.2 +++ b/src/Pure/ML/ml_context.ML	Fri Aug 23 20:35:50 2013 +0200
    14.3 @@ -74,7 +74,7 @@
    14.4    let
    14.5      val ths' = Context.>>> (Context.map_theory_result
    14.6        (Global_Theory.store_thms (Binding.name name, ths)));
    14.7 -    val _ = Context.>> (Context.map_theory (Stored_Thms.put ths'));
    14.8 +    val _ = Theory.setup (Stored_Thms.put ths');
    14.9      val _ =
   14.10        if name = "" then ()
   14.11        else if not (ML_Syntax.is_identifier name) then
   14.12 @@ -82,7 +82,7 @@
   14.13        else
   14.14          ML_Compiler.eval true Position.none
   14.15            (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
   14.16 -    val _ = Context.>> (Context.map_theory (Stored_Thms.put []));
   14.17 +    val _ = Theory.setup (Stored_Thms.put []);
   14.18    in () end;
   14.19  
   14.20  val ml_store_thms = ml_store "ML_Context.get_stored_thms";
    15.1 --- a/src/Pure/ML/ml_thms.ML	Fri Aug 23 20:09:34 2013 +0200
    15.2 +++ b/src/Pure/ML/ml_thms.ML	Fri Aug 23 20:35:50 2013 +0200
    15.3 @@ -34,23 +34,22 @@
    15.4  
    15.5  (* attribute source *)
    15.6  
    15.7 -val _ =
    15.8 -  Context.>> (Context.map_theory
    15.9 -    (ML_Context.add_antiq (Binding.name "attributes")
   15.10 -      (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
   15.11 -        let
   15.12 -          val ctxt = Context.the_proof context;
   15.13 -          val thy = Proof_Context.theory_of ctxt;
   15.14 +val _ = Theory.setup
   15.15 +  (ML_Context.add_antiq (Binding.name "attributes")
   15.16 +    (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
   15.17 +      let
   15.18 +        val ctxt = Context.the_proof context;
   15.19 +        val thy = Proof_Context.theory_of ctxt;
   15.20  
   15.21 -          val i = serial ();
   15.22 -          val srcs = map (Attrib.intern_src thy) raw_srcs;
   15.23 -          val _ = map (Attrib.attribute ctxt) srcs;
   15.24 -          val (a, ctxt') = ctxt
   15.25 -            |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
   15.26 -          val ml =
   15.27 -            ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
   15.28 -              string_of_int i ^ ";\n", "Isabelle." ^ a);
   15.29 -        in (Context.Proof ctxt', K ml) end)))));
   15.30 +        val i = serial ();
   15.31 +        val srcs = map (Attrib.intern_src thy) raw_srcs;
   15.32 +        val _ = map (Attrib.attribute ctxt) srcs;
   15.33 +        val (a, ctxt') = ctxt
   15.34 +          |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
   15.35 +        val ml =
   15.36 +          ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
   15.37 +            string_of_int i ^ ";\n", "Isabelle." ^ a);
   15.38 +      in (Context.Proof ctxt', K ml) end))));
   15.39  
   15.40  
   15.41  (* fact references *)
   15.42 @@ -73,14 +72,13 @@
   15.43        else ("", ml_body);
   15.44    in (Context.Proof ctxt'', decl) end;
   15.45  
   15.46 -val _ =
   15.47 -  Context.>> (Context.map_theory
   15.48 -    (ML_Context.add_antiq (Binding.name "thm")
   15.49 -      (Scan.depend (fn context =>
   15.50 -        Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
   15.51 -     ML_Context.add_antiq (Binding.name "thms")
   15.52 -      (Scan.depend (fn context =>
   15.53 -        Scan.pass context Attrib.thms >> thm_binding "thms" false context))));
   15.54 +val _ = Theory.setup
   15.55 +  (ML_Context.add_antiq (Binding.name "thm")
   15.56 +    (Scan.depend (fn context =>
   15.57 +      Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
   15.58 +   ML_Context.add_antiq (Binding.name "thms")
   15.59 +    (Scan.depend (fn context =>
   15.60 +      Scan.pass context Attrib.thms >> thm_binding "thms" false context)));
   15.61  
   15.62  
   15.63  (* ad-hoc goals *)
   15.64 @@ -89,9 +87,8 @@
   15.65  val by = Args.$$$ "by";
   15.66  val goal = Scan.unless (by || and_) Args.name_source;
   15.67  
   15.68 -val _ =
   15.69 -  Context.>> (Context.map_theory
   15.70 -   (ML_Context.add_antiq (Binding.name "lemma")
   15.71 +val _ = Theory.setup
   15.72 +  (ML_Context.add_antiq (Binding.name "lemma")
   15.73      (Scan.depend (fn context =>
   15.74        Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) --
   15.75        (by |-- Method.parse -- Scan.option Method.parse) >>
   15.76 @@ -111,7 +108,7 @@
   15.77              val thms =
   15.78                Proof_Context.get_fact ctxt'
   15.79                  (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
   15.80 -          in thm_binding "lemma" (length (flat propss) = 1) context thms end)))));
   15.81 +          in thm_binding "lemma" (length (flat propss) = 1) context thms end))));
   15.82  
   15.83  end;
   15.84  
    16.1 --- a/src/Pure/Proof/extraction.ML	Fri Aug 23 20:09:34 2013 +0200
    16.2 +++ b/src/Pure/Proof/extraction.ML	Fri Aug 23 20:35:50 2013 +0200
    16.3 @@ -422,7 +422,7 @@
    16.4  
    16.5  (** Pure setup **)
    16.6  
    16.7 -val _ = Context.>> (Context.map_theory
    16.8 +val _ = Theory.setup
    16.9    (add_types [("prop", ([], NONE))] #>
   16.10  
   16.11     add_typeof_eqns
   16.12 @@ -469,7 +469,7 @@
   16.13     Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
   16.14       "specify theorems to be expanded during extraction" #>
   16.15     Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
   16.16 -     "specify definitions to be expanded during extraction"));
   16.17 +     "specify definitions to be expanded during extraction");
   16.18  
   16.19  
   16.20  (**** extract program ****)
    17.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Aug 23 20:09:34 2013 +0200
    17.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Aug 23 20:35:50 2013 +0200
    17.3 @@ -190,7 +190,7 @@
    17.4    in rew' #> Option.map (rpair Proofterm.no_skel) end;
    17.5  
    17.6  fun rprocs b = [rew b];
    17.7 -val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));
    17.8 +val _ = Theory.setup (fold Proofterm.add_prf_rproc (rprocs false));
    17.9  
   17.10  
   17.11  (**** apply rewriting function to all terms in proof ****)
    18.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 20:09:34 2013 +0200
    18.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 20:35:50 2013 +0200
    18.3 @@ -807,14 +807,14 @@
    18.4  
    18.5  (* setup translations *)
    18.6  
    18.7 -val _ = Context.>> (Context.map_theory
    18.8 +val _ = Theory.setup
    18.9   (Sign.parse_ast_translation
   18.10     [("_context_const", const_ast_tr true),
   18.11      ("_context_xconst", const_ast_tr false)] #>
   18.12    Sign.typed_print_translation
   18.13     [("_type_prop", type_prop_tr'),
   18.14      ("\\<^const>TYPE", type_tr'),
   18.15 -    ("_type_constraint_", type_constraint_tr')]));
   18.16 +    ("_type_constraint_", type_constraint_tr')]);
   18.17  
   18.18  
   18.19  
    19.1 --- a/src/Pure/Thy/present.ML	Fri Aug 23 20:09:34 2013 +0200
    19.2 +++ b/src/Pure/Thy/present.ML	Fri Aug 23 20:35:50 2013 +0200
    19.3 @@ -52,8 +52,8 @@
    19.4    fun merge _ = empty;
    19.5  );
    19.6  
    19.7 -val _ = Context.>> (Context.map_theory
    19.8 -  (Browser_Info.put {chapter = Context.PureN, name = Context.PureN}));
    19.9 +val _ = Theory.setup
   19.10 +  (Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
   19.11  
   19.12  val session_name = #name o Browser_Info.get;
   19.13  val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;
    20.1 --- a/src/Pure/Thy/rail.ML	Fri Aug 23 20:09:34 2013 +0200
    20.2 +++ b/src/Pure/Thy/rail.ML	Fri Aug 23 20:35:50 2013 +0200
    20.3 @@ -263,11 +263,10 @@
    20.4  
    20.5  in
    20.6  
    20.7 -val _ =
    20.8 -  Context.>> (Context.map_theory
    20.9 -    (Thy_Output.antiquotation (Binding.name "rail")
   20.10 -      (Scan.lift (Parse.source_position Parse.string))
   20.11 -      (fn {state, ...} => output_rules state o read)));
   20.12 +val _ = Theory.setup
   20.13 +  (Thy_Output.antiquotation (Binding.name "rail")
   20.14 +    (Scan.lift (Parse.source_position Parse.string))
   20.15 +    (fn {state, ...} => output_rules state o read));
   20.16  
   20.17  end;
   20.18  
    21.1 --- a/src/Pure/Thy/term_style.ML	Fri Aug 23 20:09:34 2013 +0200
    21.2 +++ b/src/Pure/Thy/term_style.ML	Fri Aug 23 20:35:50 2013 +0200
    21.3 @@ -91,11 +91,11 @@
    21.4    | sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b)
    21.5    | sub_term t = t;
    21.6  
    21.7 -val _ = Context.>> (Context.map_theory
    21.8 +val _ = Theory.setup
    21.9   (setup "lhs" (style_lhs_rhs fst) #>
   21.10    setup "rhs" (style_lhs_rhs snd) #>
   21.11    setup "prem" style_prem #>
   21.12    setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
   21.13 -  setup "sub" (Scan.succeed (K sub_term))));
   21.14 +  setup "sub" (Scan.succeed (K sub_term)));
   21.15  
   21.16  end;
    22.1 --- a/src/Pure/Thy/thy_load.ML	Fri Aug 23 20:09:34 2013 +0200
    22.2 +++ b/src/Pure/Thy/thy_load.ML	Fri Aug 23 20:35:50 2013 +0200
    22.3 @@ -275,9 +275,8 @@
    22.4  
    22.5  (* document antiquotation *)
    22.6  
    22.7 -val _ =
    22.8 -  Context.>> (Context.map_theory
    22.9 -   (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
   22.10 +val _ = Theory.setup
   22.11 +  (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
   22.12      (fn {context = ctxt, ...} => fn (name, pos) =>
   22.13        let
   22.14          val dir = master_directory (Proof_Context.theory_of ctxt);
   22.15 @@ -290,7 +289,7 @@
   22.16          space_explode "/" name
   22.17          |> map Thy_Output.verb_text
   22.18          |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
   22.19 -      end)));
   22.20 +      end));
   22.21  
   22.22  
   22.23  (* global master path *)
    23.1 --- a/src/Pure/Thy/thy_output.ML	Fri Aug 23 20:09:34 2013 +0200
    23.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Aug 23 20:35:50 2013 +0200
    23.3 @@ -442,25 +442,24 @@
    23.4  
    23.5  (* options *)
    23.6  
    23.7 -val _ =
    23.8 -  Context.>> (Context.map_theory
    23.9 -   (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
   23.10 -    add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
   23.11 -    add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
   23.12 -    add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
   23.13 -    add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
   23.14 -    add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
   23.15 -    add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
   23.16 -    add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
   23.17 -    add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
   23.18 -    add_option (Binding.name "display") (Config.put display o boolean) #>
   23.19 -    add_option (Binding.name "break") (Config.put break o boolean) #>
   23.20 -    add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
   23.21 -    add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
   23.22 -    add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
   23.23 -    add_option (Binding.name "indent") (Config.put indent o integer) #>
   23.24 -    add_option (Binding.name "source") (Config.put source o boolean) #>
   23.25 -    add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer)));
   23.26 +val _ = Theory.setup
   23.27 + (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
   23.28 +  add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
   23.29 +  add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
   23.30 +  add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
   23.31 +  add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
   23.32 +  add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
   23.33 +  add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
   23.34 +  add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
   23.35 +  add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
   23.36 +  add_option (Binding.name "display") (Config.put display o boolean) #>
   23.37 +  add_option (Binding.name "break") (Config.put break o boolean) #>
   23.38 +  add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
   23.39 +  add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
   23.40 +  add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
   23.41 +  add_option (Binding.name "indent") (Config.put indent o integer) #>
   23.42 +  add_option (Binding.name "source") (Config.put source o boolean) #>
   23.43 +  add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer));
   23.44  
   23.45  
   23.46  (* basic pretty printing *)
   23.47 @@ -564,22 +563,21 @@
   23.48  
   23.49  in
   23.50  
   23.51 -val _ =
   23.52 -  Context.>> (Context.map_theory
   23.53 -   (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
   23.54 -    basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
   23.55 -    basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
   23.56 -    basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
   23.57 -    basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
   23.58 -    basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
   23.59 -    basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
   23.60 -    basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
   23.61 -    basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
   23.62 -    basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
   23.63 -    basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
   23.64 -    basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
   23.65 -    basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
   23.66 -    basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory));
   23.67 +val _ = Theory.setup
   23.68 + (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
   23.69 +  basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
   23.70 +  basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
   23.71 +  basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
   23.72 +  basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
   23.73 +  basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
   23.74 +  basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
   23.75 +  basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
   23.76 +  basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
   23.77 +  basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
   23.78 +  basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
   23.79 +  basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
   23.80 +  basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
   23.81 +  basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);
   23.82  
   23.83  end;
   23.84  
   23.85 @@ -600,10 +598,9 @@
   23.86  
   23.87  in
   23.88  
   23.89 -val _ =
   23.90 -  Context.>> (Context.map_theory
   23.91 -   (goal_state (Binding.name "goals") true #>
   23.92 -    goal_state (Binding.name "subgoals") false));
   23.93 +val _ = Theory.setup
   23.94 + (goal_state (Binding.name "goals") true #>
   23.95 +  goal_state (Binding.name "subgoals") false);
   23.96  
   23.97  end;
   23.98  
   23.99 @@ -612,9 +609,8 @@
  23.100  
  23.101  val _ = Keyword.define ("by", NONE);  (*overlap with command category*)
  23.102  
  23.103 -val _ =
  23.104 -  Context.>> (Context.map_theory
  23.105 -   (antiquotation (Binding.name "lemma")
  23.106 +val _ = Theory.setup
  23.107 +  (antiquotation (Binding.name "lemma")
  23.108      (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
  23.109      (fn {source, context, ...} => fn (prop, methods) =>
  23.110        let
  23.111 @@ -624,7 +620,7 @@
  23.112          val _ = context
  23.113            |> Proof.theorem NONE (K I) [[(prop, [])]]
  23.114            |> Proof.global_terminal_proof methods;
  23.115 -      in output context (maybe_pretty_source pretty_term context prop_src [prop]) end)));
  23.116 +      in output context (maybe_pretty_source pretty_term context prop_src [prop]) end));
  23.117  
  23.118  
  23.119  (* ML text *)
  23.120 @@ -649,20 +645,19 @@
  23.121  
  23.122  in
  23.123  
  23.124 -val _ =
  23.125 -  Context.>> (Context.map_theory
  23.126 -   (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
  23.127 -    ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
  23.128 -    ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
  23.129 -    ml_text (Binding.name "ML_struct")
  23.130 -      (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
  23.131 +val _ = Theory.setup
  23.132 + (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
  23.133 +  ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
  23.134 +  ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
  23.135 +  ml_text (Binding.name "ML_struct")
  23.136 +    (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
  23.137  
  23.138 -    ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
  23.139 -      (fn pos => fn txt =>
  23.140 -        ML_Lex.read Position.none ("ML_Env.check_functor " ^
  23.141 -          ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
  23.142 +  ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
  23.143 +    (fn pos => fn txt =>
  23.144 +      ML_Lex.read Position.none ("ML_Env.check_functor " ^
  23.145 +        ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
  23.146  
  23.147 -    ml_text (Binding.name "ML_text") (K (K []))));
  23.148 +  ml_text (Binding.name "ML_text") (K (K [])));
  23.149  
  23.150  end;
  23.151  
    24.1 --- a/src/Pure/axclass.ML	Fri Aug 23 20:09:34 2013 +0200
    24.2 +++ b/src/Pure/axclass.ML	Fri Aug 23 20:35:50 2013 +0200
    24.3 @@ -264,9 +264,8 @@
    24.4      else SOME (map_proven_arities (K arities') thy)
    24.5    end;
    24.6  
    24.7 -val _ = Context.>> (Context.map_theory
    24.8 -  (Theory.at_begin complete_classrels #>
    24.9 -   Theory.at_begin complete_arities));
   24.10 +val _ = Theory.setup
   24.11 +  (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities);
   24.12  
   24.13  val _ = Proofterm.install_axclass_proofs
   24.14    {classrel_proof = Thm.proof_of oo the_classrel,
    25.1 --- a/src/Pure/pure_thy.ML	Fri Aug 23 20:09:34 2013 +0200
    25.2 +++ b/src/Pure/pure_thy.ML	Fri Aug 23 20:35:50 2013 +0200
    25.3 @@ -56,7 +56,7 @@
    25.4  val token_markers =
    25.5    ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
    25.6  
    25.7 -val _ = Context.>> (Context.map_theory
    25.8 +val _ = Theory.setup
    25.9    (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
   25.10     Old_Appl_Syntax.put false #>
   25.11     Sign.add_types_global
   25.12 @@ -221,6 +221,6 @@
   25.13    #> Sign.hide_const false "Pure.conjunction"
   25.14    #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
   25.15    #> fold (fn (a, prop) =>
   25.16 -      snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms));
   25.17 +      snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms);
   25.18  
   25.19  end;
    26.1 --- a/src/Pure/simplifier.ML	Fri Aug 23 20:09:34 2013 +0200
    26.2 +++ b/src/Pure/simplifier.ML	Fri Aug 23 20:35:50 2013 +0200
    26.3 @@ -129,10 +129,10 @@
    26.4  (* global simprocs *)
    26.5  
    26.6  fun Addsimprocs args =
    26.7 -  Context.>> (Context.map_theory (map_theory_simpset (fn ctxt => ctxt addsimprocs args)));
    26.8 +  Theory.setup (map_theory_simpset (fn ctxt => ctxt addsimprocs args));
    26.9  
   26.10  fun Delsimprocs args =
   26.11 -  Context.>> (Context.map_theory (map_theory_simpset (fn ctxt => ctxt delsimprocs args)));
   26.12 +  Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs args));
   26.13  
   26.14  
   26.15  
   26.16 @@ -154,13 +154,11 @@
   26.17  fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
   26.18  val the_simproc = Name_Space.get o get_simprocs;
   26.19  
   26.20 -val _ =
   26.21 -  Context.>> (Context.map_theory
   26.22 -   (ML_Antiquote.value (Binding.name "simproc")
   26.23 -      (Args.context -- Scan.lift (Parse.position Args.name)
   26.24 -        >> (fn (ctxt, name) =>
   26.25 -          "Simplifier.the_simproc ML_context " ^
   26.26 -            ML_Syntax.print_string (check_simproc ctxt name)))));
   26.27 +val _ = Theory.setup
   26.28 +  (ML_Antiquote.value (Binding.name "simproc")
   26.29 +    (Args.context -- Scan.lift (Parse.position Args.name)
   26.30 +      >> (fn (ctxt, name) =>
   26.31 +        "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
   26.32  
   26.33  
   26.34  (* define simprocs *)
   26.35 @@ -327,14 +325,14 @@
   26.36  
   26.37  (* setup attributes *)
   26.38  
   26.39 -val _ = Context.>> (Context.map_theory
   26.40 +val _ = Theory.setup
   26.41   (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
   26.42      "declaration of Simplifier rewrite rule" #>
   26.43    Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
   26.44      "declaration of Simplifier congruence rule" #>
   26.45    Attrib.setup (Binding.name "simproc") simproc_att
   26.46      "declaration of simplification procedures" #>
   26.47 -  Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
   26.48 +  Attrib.setup (Binding.name "simplified") simplified "simplified rule");
   26.49  
   26.50  
   26.51  
    27.1 --- a/src/Pure/theory.ML	Fri Aug 23 20:09:34 2013 +0200
    27.2 +++ b/src/Pure/theory.ML	Fri Aug 23 20:35:50 2013 +0200
    27.3 @@ -15,6 +15,7 @@
    27.4    val merge: theory * theory -> theory
    27.5    val merge_list: theory list -> theory
    27.6    val requires: theory -> string -> string -> unit
    27.7 +  val setup: (theory -> theory) -> unit
    27.8    val get_markup: theory -> Markup.T
    27.9    val axiom_space: theory -> Name_Space.T
   27.10    val axiom_table: theory -> term Symtab.table
   27.11 @@ -59,6 +60,8 @@
   27.12    if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then ()
   27.13    else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   27.14  
   27.15 +fun setup f = Context.>> (Context.map_theory f);
   27.16 +
   27.17  
   27.18  
   27.19  (** datatype thy **)
    28.1 --- a/src/Tools/Code/code_runtime.ML	Fri Aug 23 20:09:34 2013 +0200
    28.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Aug 23 20:35:50 2013 +0200
    28.3 @@ -51,14 +51,14 @@
    28.4  
    28.5  datatype truth = Holds;
    28.6  
    28.7 -val _ = Context.>> (Context.map_theory
    28.8 +val _ = Theory.setup
    28.9    (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
   28.10    #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
   28.11      [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
   28.12    #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
   28.13      [(target, SOME (Code_Printer.plain_const_syntax s_Holds))]))
   28.14    #> Code_Target.add_reserved target this
   28.15 -  #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
   28.16 +  #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
   28.17         (*avoid further pervasive infix names*)
   28.18  
   28.19  val trace = Unsynchronized.ref false;
   28.20 @@ -345,10 +345,9 @@
   28.21  
   28.22  (** Isar setup **)
   28.23  
   28.24 -val _ =
   28.25 -  Context.>> (Context.map_theory
   28.26 -    (ML_Context.add_antiq @{binding code}
   28.27 -      (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context))));
   28.28 +val _ = Theory.setup
   28.29 +  (ML_Context.add_antiq @{binding code}
   28.30 +    (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context)));
   28.31  
   28.32  local
   28.33  
   28.34 @@ -387,7 +386,7 @@
   28.35  fun notify_val (string, value) = 
   28.36    let
   28.37      val _ = #enterVal ML_Env.name_space (string, value);
   28.38 -    val _ = Context.>> ((Context.map_theory o Loaded_Values.map) (insert (op =) string));
   28.39 +    val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
   28.40    in () end;
   28.41  
   28.42  fun abort _ = error "Only value bindings allowed.";
    29.1 --- a/src/Tools/Spec_Check/output_style.ML	Fri Aug 23 20:09:34 2013 +0200
    29.2 +++ b/src/Tools/Spec_Check/output_style.ML	Fri Aug 23 20:35:50 2013 +0200
    29.3 @@ -78,6 +78,8 @@
    29.4          {status = status, finish = finish}
    29.5        end)
    29.6  
    29.7 +val _ = Theory.setup perl_style;
    29.8 +
    29.9  
   29.10  (* CM style: meshes with CM output; highlighted in sml-mode *)
   29.11  
   29.12 @@ -106,9 +108,6 @@
   29.13          {status = K (), finish = finish}
   29.14        end)
   29.15  
   29.16 -
   29.17 -(* setup *)
   29.18 -
   29.19 -val _ = Context.>> (Context.map_theory (perl_style #> cm_style));
   29.20 +val _ = Theory.setup cm_style;
   29.21  
   29.22  end
    30.1 --- a/src/Tools/try.ML	Fri Aug 23 20:09:34 2013 +0200
    30.2 +++ b/src/Tools/try.ML	Fri Aug 23 20:35:50 2013 +0200
    30.3 @@ -142,7 +142,6 @@
    30.4  
    30.5  (* hybrid tool setup *)
    30.6  
    30.7 -fun tool_setup tool =
    30.8 -  (Context.>> (Context.map_theory (register_tool tool)); print_function tool)
    30.9 +fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool)
   30.10  
   30.11  end;