1.1 --- a/doc-src/IsarImplementation/Thy/integration.thy	Fri Mar 28 19:43:54 2008 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/integration.thy	Fri Mar 28 20:02:04 2008 +0100
     1.3 @@ -241,7 +241,7 @@
     1.4  text %mlref {*
     1.5    \begin{mldecls}
     1.6    @{index_ML the_context: "unit -> theory"} \\
     1.7 -  @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
     1.8 +  @{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\
     1.9    \end{mldecls}
    1.10  
    1.11    \begin{description}
    1.12 @@ -255,13 +255,8 @@
    1.13    information immediately, or produce an explicit @{ML_type
    1.14    theory_ref} (cf.\ \secref{sec:context-theory}).
    1.15  
    1.16 -  \item @{ML "Context.>>"}~@{text f} applies theory transformation
    1.17 -  @{text f} to the current theory of the {\ML} toplevel.  In order to
    1.18 -  work as expected, the theory should be still under construction, and
    1.19 -  the Isar language element that invoked the {\ML} compiler in the
    1.20 -  first place should be ready to accept the changed theory value
    1.21 -  (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
    1.22 -  Otherwise the theory becomes stale!
    1.23 +  \item @{ML "Context.>>"}~@{text f} applies context transformation
    1.24 +  @{text f} to the implicit context of the {\ML} toplevel.
    1.25  
    1.26    \end{description}
    1.27  

     2.1 --- a/src/Pure/Isar/attrib.ML	Fri Mar 28 19:43:54 2008 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Fri Mar 28 20:02:04 2008 +0100
     2.3 @@ -276,7 +276,7 @@
     2.4  
     2.5  (* theory setup *)
     2.6  
     2.7 -val _ = Context.>>
     2.8 +val _ = Context.>> (Context.map_theory
     2.9   (add_attributes
    2.10     [("attribute", internal_att, "internal attribute"),
    2.11      ("tagged", tagged, "tagged theorem"),
    2.12 @@ -301,7 +301,7 @@
    2.13      ("rule_format", rule_format, "result put into standard rule format"),
    2.14      ("rotated", rotated, "rotated theorem premises"),
    2.15      ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
    2.16 -      "declaration of definitional transformations")]);
    2.17 +      "declaration of definitional transformations")]));
    2.18  
    2.19  
    2.20  
    2.21 @@ -379,12 +379,12 @@
    2.22  
    2.23  (* theory setup *)
    2.24  
    2.25 -val _ = Context.>>
    2.26 +val _ = Context.>> (Context.map_theory
    2.27   (register_config Unify.trace_bound_value #>
    2.28    register_config Unify.search_bound_value #>
    2.29    register_config Unify.trace_simp_value #>
    2.30    register_config Unify.trace_types_value #>
    2.31 -  register_config MetaSimplifier.simp_depth_limit_value);
    2.32 +  register_config MetaSimplifier.simp_depth_limit_value));
    2.33  
    2.34  end;
    2.35  

     3.1 --- a/src/Pure/Isar/calculation.ML	Fri Mar 28 19:43:54 2008 +0100
     3.2 +++ b/src/Pure/Isar/calculation.ML	Fri Mar 28 20:02:04 2008 +0100
     3.3 @@ -92,14 +92,14 @@
     3.4  val trans_att = Attrib.add_del_args trans_add trans_del;
     3.5  val sym_att = Attrib.add_del_args sym_add sym_del;
     3.6  
     3.7 -val _ = Context.>>
     3.8 +val _ = Context.>> (Context.map_theory
     3.9   (Attrib.add_attributes
    3.10     [("trans", trans_att, "declaration of transitivity rule"),
    3.11      ("sym", sym_att, "declaration of symmetry rule"),
    3.12      ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
    3.13    PureThy.add_thms
    3.14     [(("", transitive_thm), [trans_add]),
    3.15 -    (("", symmetric_thm), [sym_add])] #> snd);
    3.16 +    (("", symmetric_thm), [sym_add])] #> snd));
    3.17  
    3.18  
    3.19  

     4.1 --- a/src/Pure/Isar/class.ML	Fri Mar 28 19:43:54 2008 +0100
     4.2 +++ b/src/Pure/Isar/class.ML	Fri Mar 28 20:02:04 2008 +0100
     4.3 @@ -140,7 +140,7 @@
     4.4  fun mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
     4.5      (defs, operations)) =
     4.6    ClassData { consts = consts, base_sort = base_sort, inst = inst,
     4.7 -    morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom, 
     4.8 +    morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
     4.9      defs = defs, operations = operations };
    4.10  fun map_class_data f (ClassData { consts, base_sort, inst, morphism,
    4.11      assm_intro, of_class, axiom, defs, operations }) =
    4.12 @@ -304,7 +304,7 @@
    4.13        #> map_types subst_typ;
    4.14      fun subst_thm defs = Drule.standard' #> instantiate_class #> lift_axiom
    4.15        #> MetaSimplifier.rewrite_rule defs;
    4.16 -    fun morphism thy defs = 
    4.17 +    fun morphism thy defs =
    4.18        Morphism.typ_morphism subst_typ
    4.19        $> Morphism.term_morphism (subst_term thy defs)
    4.20        $> Morphism.thm_morphism (subst_thm defs);
    4.21 @@ -395,11 +395,13 @@
    4.22    HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
    4.23      default_intro_classes_tac facts;
    4.24  
    4.25 -val _ = Context.>> (Method.add_methods
    4.26 - [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    4.27 -    "back-chain introduction rules of classes"),
    4.28 -  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
    4.29 -    "apply some intro/elim rule")]);
    4.30 +val _ = Context.>> (Context.map_theory
    4.31 +  (Method.add_methods
    4.32 +   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    4.33 +      "back-chain introduction rules of classes"),
    4.34 +    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
    4.35 +      "apply some intro/elim rule")]));
    4.36 +
    4.37  
    4.38  
    4.39  (** classes and class target **)

     5.1 --- a/src/Pure/Isar/code.ML	Fri Mar 28 19:43:54 2008 +0100
     5.2 +++ b/src/Pure/Isar/code.ML	Fri Mar 28 20:02:04 2008 +0100
     5.3 @@ -107,8 +107,9 @@
     5.4      val code_attr = Attrib.syntax (Scan.peek (fn context =>
     5.5        List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
     5.6    in
     5.7 -    Context.>> (Attrib.add_attributes
     5.8 -      [("code", code_attr, "declare theorems for code generation")])
     5.9 +    Context.>> (Context.map_theory
    5.10 +      (Attrib.add_attributes
    5.11 +        [("code", code_attr, "declare theorems for code generation")]))
    5.12    end;
    5.13  
    5.14  
    5.15 @@ -387,7 +388,7 @@
    5.16      in (exec, ref data) end;
    5.17  );
    5.18  
    5.19 -val _ = Context.>> CodeData.init;
    5.20 +val _ = Context.>> (Context.map_theory CodeData.init);
    5.21  
    5.22  fun thy_data f thy = f ((snd o CodeData.get) thy);
    5.23  
    5.24 @@ -864,7 +865,7 @@
    5.25      (remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
    5.26          (*fully applied in order to get right context for mk_rew!*)
    5.27  
    5.28 -val _ = Context.>>
    5.29 +val _ = Context.>> (Context.map_theory
    5.30    (let
    5.31      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    5.32      fun add_simple_attribute (name, f) =
    5.33 @@ -877,7 +878,7 @@
    5.34      #> add_del_attribute ("func", (add_func, del_func))
    5.35      #> add_del_attribute ("inline", (add_inline, del_inline))
    5.36      #> add_del_attribute ("post", (add_post, del_post))
    5.37 -  end);
    5.38 +  end));
    5.39  
    5.40  
    5.41  (** post- and preprocessing **)

     6.1 --- a/src/Pure/Isar/context_rules.ML	Fri Mar 28 19:43:54 2008 +0100
     6.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Mar 28 20:02:04 2008 +0100
     6.3 @@ -198,8 +198,8 @@
     6.4  val elim_query  = rule_add elim_queryK I;
     6.5  val dest_query  = rule_add elim_queryK Tactic.make_elim;
     6.6  
     6.7 -val _ = Context.>>
     6.8 -  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
     6.9 +val _ = Context.>> (Context.map_theory
    6.10 +  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]));
    6.11  
    6.12  
    6.13  (* concrete syntax *)
    6.14 @@ -215,6 +215,6 @@
    6.15    ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
    6.16      "remove declaration of intro/elim/dest rule")];
    6.17  
    6.18 -val _ = Context.>> (Attrib.add_attributes rule_atts);
    6.19 +val _ = Context.>> (Context.map_theory (Attrib.add_attributes rule_atts));
    6.20  
    6.21  end;

     7.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Mar 28 19:43:54 2008 +0100
     7.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Mar 28 20:02:04 2008 +0100
     7.3 @@ -204,7 +204,8 @@
     7.4      \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
     7.5      \  val name = " ^ quote name ^ ";\n\
     7.6      \  exception Arg of T;\n\
     7.7 -    \  val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
     7.8 +    \  val _ = Context.>> (Context.map_theory\n\
     7.9 +    \    (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\
    7.10      \  val thy = ML_Context.the_global_context ();\n\
    7.11      \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
    7.12      \in\n\

     8.1 --- a/src/Pure/Isar/locale.ML	Fri Mar 28 19:43:54 2008 +0100
     8.2 +++ b/src/Pure/Isar/locale.ML	Fri Mar 28 20:02:04 2008 +0100
     8.3 @@ -2000,11 +2000,11 @@
     8.4  
     8.5  end;
     8.6  
     8.7 -val _ = Context.>>
     8.8 +val _ = Context.>> (Context.map_theory
     8.9   (add_locale_i (SOME "") "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
    8.10    snd #> ProofContext.theory_of #>
    8.11    add_locale_i (SOME "") "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
    8.12 -  snd #> ProofContext.theory_of);
    8.13 +  snd #> ProofContext.theory_of));
    8.14  
    8.15  
    8.16  
    8.17 @@ -2041,13 +2041,14 @@
    8.18      Method.intros_tac (wits @ intros) facts st
    8.19    end;
    8.20  
    8.21 -val _ = Context.>> (Method.add_methods
    8.22 -  [("intro_locales",
    8.23 -    Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
    8.24 -    "back-chain introduction rules of locales without unfolding predicates"),
    8.25 -   ("unfold_locales",
    8.26 -    Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
    8.27 -    "back-chain all introduction rules of locales")]);
    8.28 +val _ = Context.>> (Context.map_theory
    8.29 +  (Method.add_methods
    8.30 +    [("intro_locales",
    8.31 +      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
    8.32 +      "back-chain introduction rules of locales without unfolding predicates"),
    8.33 +     ("unfold_locales",
    8.34 +      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
    8.35 +      "back-chain all introduction rules of locales")]));
    8.36  
    8.37  end;
    8.38  

     9.1 --- a/src/Pure/Isar/method.ML	Fri Mar 28 19:43:54 2008 +0100
     9.2 +++ b/src/Pure/Isar/method.ML	Fri Mar 28 20:02:04 2008 +0100
     9.3 @@ -554,31 +554,33 @@
     9.4  
     9.5  (* theory setup *)
     9.6  
     9.7 -val _ = Context.>> (add_methods
     9.8 - [("fail", no_args fail, "force failure"),
     9.9 -  ("succeed", no_args succeed, "succeed"),
    9.10 -  ("-", no_args insert_facts, "do nothing (insert current facts only)"),
    9.11 -  ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
    9.12 -  ("intro", thms_args intro, "repeatedly apply introduction rules"),
    9.13 -  ("elim", thms_args elim, "repeatedly apply elimination rules"),
    9.14 -  ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"),
    9.15 -  ("fold", thms_ctxt_args fold_meth, "fold definitions"),
    9.16 -  ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
    9.17 -    "present local premises as object-level statements"),
    9.18 -  ("iprover", iprover_meth, "intuitionistic proof search"),
    9.19 -  ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
    9.20 -  ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
    9.21 -  ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
    9.22 -  ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
    9.23 -  ("this", no_args this, "apply current facts as rules"),
    9.24 -  ("fact", thms_ctxt_args fact, "composition by facts from context"),
    9.25 -  ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
    9.26 -  ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
    9.27 -    "rename parameters of goal"),
    9.28 -  ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
    9.29 -    "rotate assumptions of goal"),
    9.30 -  ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"),
    9.31 -  ("raw_tactic", simple_args (Args.position Args.name) raw_tactic, "ML tactic as raw proof method")]);
    9.32 +val _ = Context.>> (Context.map_theory
    9.33 +  (add_methods
    9.34 +   [("fail", no_args fail, "force failure"),
    9.35 +    ("succeed", no_args succeed, "succeed"),
    9.36 +    ("-", no_args insert_facts, "do nothing (insert current facts only)"),
    9.37 +    ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
    9.38 +    ("intro", thms_args intro, "repeatedly apply introduction rules"),
    9.39 +    ("elim", thms_args elim, "repeatedly apply elimination rules"),
    9.40 +    ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"),
    9.41 +    ("fold", thms_ctxt_args fold_meth, "fold definitions"),
    9.42 +    ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
    9.43 +      "present local premises as object-level statements"),
    9.44 +    ("iprover", iprover_meth, "intuitionistic proof search"),
    9.45 +    ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
    9.46 +    ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
    9.47 +    ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
    9.48 +    ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
    9.49 +    ("this", no_args this, "apply current facts as rules"),
    9.50 +    ("fact", thms_ctxt_args fact, "composition by facts from context"),
    9.51 +    ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
    9.52 +    ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
    9.53 +      "rename parameters of goal"),
    9.54 +    ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
    9.55 +      "rotate assumptions of goal"),
    9.56 +    ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"),
    9.57 +    ("raw_tactic", simple_args (Args.position Args.name) raw_tactic,
    9.58 +      "ML tactic as raw proof method")]));
    9.59  
    9.60  
    9.61  (* outer parser *)

    10.1 --- a/src/Pure/Isar/object_logic.ML	Fri Mar 28 19:43:54 2008 +0100
    10.2 +++ b/src/Pure/Isar/object_logic.ML	Fri Mar 28 20:02:04 2008 +0100
    10.3 @@ -193,7 +193,7 @@
    10.4  val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
    10.5  val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
    10.6  
    10.7 -val _ = Context.>> (add_rulify Drule.norm_hhf_eq);
    10.8 +val _ = Context.>> (Context.map_theory (add_rulify Drule.norm_hhf_eq));
    10.9  
   10.10  
   10.11  (* atomize *)

    11.1 --- a/src/Pure/Isar/proof_context.ML	Fri Mar 28 19:43:54 2008 +0100
    11.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Mar 28 20:02:04 2008 +0100
    11.3 @@ -571,9 +571,8 @@
    11.4  fun standard_term_uncheck ctxt =
    11.5    map (contract_abbrevs ctxt);
    11.6  
    11.7 -fun add eq what f = Context.>>
    11.8 -  (Context.theory_map (what (fn xs => fn ctxt =>
    11.9 -    let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end)));
   11.10 +fun add eq what f = Context.>> (what (fn xs => fn ctxt =>
   11.11 +  let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end));
   11.12  
   11.13  in
   11.14  
   11.15 @@ -922,14 +921,14 @@
   11.16  
   11.17  in
   11.18  
   11.19 -val _ = Context.>>
   11.20 +val _ = Context.>> (Context.map_theory
   11.21   (Sign.add_syntax
   11.22     [("_context_const", "id => 'a", Delimfix "CONST _"),
   11.23      ("_context_const", "longid => 'a", Delimfix "CONST _"),
   11.24      ("_context_xconst", "id => 'a", Delimfix "XCONST _"),
   11.25      ("_context_xconst", "longid => 'a", Delimfix "XCONST _")] #>
   11.26    Sign.add_advanced_trfuns
   11.27 -    ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], []));
   11.28 +    ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
   11.29  
   11.30  end;
   11.31  

    12.1 --- a/src/Pure/Isar/rule_insts.ML	Fri Mar 28 19:43:54 2008 +0100
    12.2 +++ b/src/Pure/Isar/rule_insts.ML	Fri Mar 28 20:02:04 2008 +0100
    12.3 @@ -218,9 +218,10 @@
    12.4  
    12.5  (* setup *)
    12.6  
    12.7 -val _ = Context.>> (Attrib.add_attributes
    12.8 - [("where", where_att, "named instantiation of theorem"),
    12.9 -  ("of", of_att, "positional instantiation of theorem")]);
   12.10 +val _ = Context.>> (Context.map_theory
   12.11 +  (Attrib.add_attributes
   12.12 +   [("where", where_att, "named instantiation of theorem"),
   12.13 +    ("of", of_att, "positional instantiation of theorem")]));
   12.14  
   12.15  
   12.16  
   12.17 @@ -367,21 +368,22 @@
   12.18  
   12.19  (* setup *)
   12.20  
   12.21 -val _ = Context.>> (Method.add_methods
   12.22 - [("rule_tac", inst_args_var res_inst_meth,
   12.23 -    "apply rule (dynamic instantiation)"),
   12.24 -  ("erule_tac", inst_args_var eres_inst_meth,
   12.25 -    "apply rule in elimination manner (dynamic instantiation)"),
   12.26 -  ("drule_tac", inst_args_var dres_inst_meth,
   12.27 -    "apply rule in destruct manner (dynamic instantiation)"),
   12.28 -  ("frule_tac", inst_args_var forw_inst_meth,
   12.29 -    "apply rule in forward manner (dynamic instantiation)"),
   12.30 -  ("cut_tac", inst_args_var cut_inst_meth,
   12.31 -    "cut rule (dynamic instantiation)"),
   12.32 -  ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
   12.33 -    "insert subgoal (dynamic instantiation)"),
   12.34 -  ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
   12.35 -    "remove premise (dynamic instantiation)")]);
   12.36 +val _ = Context.>> (Context.map_theory
   12.37 +  (Method.add_methods
   12.38 +   [("rule_tac", inst_args_var res_inst_meth,
   12.39 +      "apply rule (dynamic instantiation)"),
   12.40 +    ("erule_tac", inst_args_var eres_inst_meth,
   12.41 +      "apply rule in elimination manner (dynamic instantiation)"),
   12.42 +    ("drule_tac", inst_args_var dres_inst_meth,
   12.43 +      "apply rule in destruct manner (dynamic instantiation)"),
   12.44 +    ("frule_tac", inst_args_var forw_inst_meth,
   12.45 +      "apply rule in forward manner (dynamic instantiation)"),
   12.46 +    ("cut_tac", inst_args_var cut_inst_meth,
   12.47 +      "cut rule (dynamic instantiation)"),
   12.48 +    ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
   12.49 +      "insert subgoal (dynamic instantiation)"),
   12.50 +    ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
   12.51 +      "remove premise (dynamic instantiation)")]));
   12.52  
   12.53  end;
   12.54  

    13.1 --- a/src/Pure/Isar/skip_proof.ML	Fri Mar 28 19:43:54 2008 +0100
    13.2 +++ b/src/Pure/Isar/skip_proof.ML	Fri Mar 28 20:02:04 2008 +0100
    13.3 @@ -24,7 +24,8 @@
    13.4    if ! quick_and_dirty then prop
    13.5    else error "Proof may be skipped in quick_and_dirty mode only!";
    13.6  
    13.7 -val _ = Context.>> (Theory.add_oracle ("skip_proof", skip_proof));
    13.8 +val _ = Context.>> (Context.map_theory
    13.9 +  (Theory.add_oracle ("skip_proof", skip_proof)));
   13.10  
   13.11  
   13.12  (* basic cheating *)

    14.1 --- a/src/Pure/Proof/extraction.ML	Fri Mar 28 19:43:54 2008 +0100
    14.2 +++ b/src/Pure/Proof/extraction.ML	Fri Mar 28 20:02:04 2008 +0100
    14.3 @@ -395,7 +395,7 @@
    14.4  
    14.5  (** Pure setup **)
    14.6  
    14.7 -val _ = Context.>>
    14.8 +val _ = Context.>> (Context.map_theory
    14.9    (add_types [("prop", ([], NONE))] #>
   14.10  
   14.11     add_typeof_eqns
   14.12 @@ -441,7 +441,7 @@
   14.13  
   14.14     Attrib.add_attributes
   14.15       [("extraction_expand", extraction_expand,
   14.16 -       "specify theorems / definitions to be expanded during extraction")]);
   14.17 +       "specify theorems / definitions to be expanded during extraction")]));
   14.18  
   14.19  
   14.20  (**** extract program ****)

    15.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 28 19:43:54 2008 +0100
    15.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 28 20:02:04 2008 +0100
    15.3 @@ -187,7 +187,7 @@
    15.4    in rew' end;
    15.5  
    15.6  fun rprocs b = [("Pure/meta_equality", rew b)];
    15.7 -val _ = Context.>> (fold Proofterm.add_prf_rproc (rprocs false));
    15.8 +val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));
    15.9  
   15.10  
   15.11  (**** apply rewriting function to all terms in proof ****)

    16.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Mar 28 19:43:54 2008 +0100
    16.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Mar 28 20:02:04 2008 +0100
    16.3 @@ -92,7 +92,7 @@
    16.4  
    16.5  in
    16.6  
    16.7 -val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
    16.8 +val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns proof_general_trans));
    16.9  
   16.10  end;
   16.11  

    17.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Mar 28 19:43:54 2008 +0100
    17.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Mar 28 20:02:04 2008 +0100
    17.3 @@ -105,7 +105,7 @@
    17.4  
    17.5  in
    17.6  
    17.7 -val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
    17.8 +val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns proof_general_trans));
    17.9  
   17.10  end;
   17.11  

    18.1 --- a/src/Pure/Thy/html.ML	Fri Mar 28 19:43:54 2008 +0100
    18.2 +++ b/src/Pure/Thy/html.ML	Fri Mar 28 20:02:04 2008 +0100
    18.3 @@ -267,7 +267,8 @@
    18.4    ("var",   var_or_skolem),
    18.5    ("xstr",  style "xstr")];
    18.6  
    18.7 -val _ = Context.>> (Sign.add_mode_tokentrfuns htmlN html_trans);
    18.8 +val _ = Context.>> (Context.map_theory
    18.9 +  (Sign.add_mode_tokentrfuns htmlN html_trans));
   18.10  
   18.11  
   18.12  

    19.1 --- a/src/Pure/Thy/term_style.ML	Fri Mar 28 19:43:54 2008 +0100
    19.2 +++ b/src/Pure/Thy/term_style.ML	Fri Mar 28 20:02:04 2008 +0100
    19.3 @@ -65,7 +65,7 @@
    19.4        " in propositon: " ^ Syntax.string_of_term ctxt t)
    19.5    end;
    19.6  
    19.7 -val _ = Context.>>
    19.8 +val _ = Context.>> (Context.map_theory
    19.9   (add_style "lhs" (fst oo style_binargs) #>
   19.10    add_style "rhs" (snd oo style_binargs) #>
   19.11    add_style "prem1" (style_parm_premise 1) #>
   19.12 @@ -87,6 +87,6 @@
   19.13    add_style "prem17" (style_parm_premise 17) #>
   19.14    add_style "prem18" (style_parm_premise 18) #>
   19.15    add_style "prem19" (style_parm_premise 19) #>
   19.16 -  add_style "concl" (K Logic.strip_imp_concl));
   19.17 +  add_style "concl" (K Logic.strip_imp_concl)));
   19.18  
   19.19  end;

    20.1 --- a/src/Pure/Tools/isabelle_process.ML	Fri Mar 28 19:43:54 2008 +0100
    20.2 +++ b/src/Pure/Tools/isabelle_process.ML	Fri Mar 28 20:02:04 2008 +0100
    20.3 @@ -160,7 +160,7 @@
    20.4  
    20.5  in
    20.6  
    20.7 -val _ = Context.>> (Sign.add_tokentrfuns token_trans);
    20.8 +val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans));
    20.9  
   20.10  end;
   20.11  

    21.1 --- a/src/Pure/assumption.ML	Fri Mar 28 19:43:54 2008 +0100
    21.2 +++ b/src/Pure/assumption.ML	Fri Mar 28 20:02:04 2008 +0100
    21.3 @@ -79,8 +79,8 @@
    21.4  (* named prems -- legacy feature *)
    21.5  
    21.6  val _ = Context.>>
    21.7 -  (PureThy.add_thms_dynamic ("prems",
    21.8 -    fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt));
    21.9 +  (Context.map_theory (PureThy.add_thms_dynamic ("prems",
   21.10 +    fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
   21.11  
   21.12  
   21.13  (* add assumptions *)

    22.1 --- a/src/Pure/codegen.ML	Fri Mar 28 19:43:54 2008 +0100
    22.2 +++ b/src/Pure/codegen.ML	Fri Mar 28 20:02:04 2008 +0100
    22.3 @@ -343,8 +343,8 @@
    22.4    (let
    22.5      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    22.6    in
    22.7 -    Code.add_attribute ("unfold", Scan.succeed (mk_attribute
    22.8 -      (fn thm => add_unfold thm #> Code.add_inline thm)))
    22.9 +    Context.map_theory (Code.add_attribute ("unfold", Scan.succeed (mk_attribute
   22.10 +      (fn thm => add_unfold thm #> Code.add_inline thm))))
   22.11    end);
   22.12  
   22.13  
   22.14 @@ -786,9 +786,9 @@
   22.15                   (add_edge (node_id, dep) gr'', p module''))
   22.16             end);
   22.17  
   22.18 -val _ = Context.>>
   22.19 +val _ = Context.>> (Context.map_theory
   22.20   (add_codegen "default" default_codegen #>
   22.21 -  add_tycodegen "default" default_tycodegen);
   22.22 +  add_tycodegen "default" default_tycodegen));
   22.23  
   22.24  
   22.25  fun mk_tuple [p] = p
   22.26 @@ -1026,8 +1026,7 @@
   22.27      else state
   22.28    end;
   22.29  
   22.30 -val _ = Context.>>
   22.31 -  (Context.theory_map (Specification.add_theorem_hook test_goal'));
   22.32 +val _ = Context.>> (Specification.add_theorem_hook test_goal');
   22.33  
   22.34  
   22.35  (**** Evaluator for terms ****)
   22.36 @@ -1078,8 +1077,8 @@
   22.37    let val {thy, t, ...} = rep_cterm ct
   22.38    in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
   22.39  
   22.40 -val _ = Context.>>
   22.41 -  (Theory.add_oracle ("evaluation", evaluation_oracle));
   22.42 +val _ = Context.>> (Context.map_theory
   22.43 +  (Theory.add_oracle ("evaluation", evaluation_oracle)));
   22.44  
   22.45  
   22.46  (**** Interface ****)

    23.1 --- a/src/Pure/compress.ML	Fri Mar 28 19:43:54 2008 +0100
    23.2 +++ b/src/Pure/compress.ML	Fri Mar 28 20:02:04 2008 +0100
    23.3 @@ -30,7 +30,7 @@
    23.4      ref (Termtab.merge (K true) (terms1, terms2)));
    23.5  );
    23.6  
    23.7 -val _ = Context.>> CompressData.init;
    23.8 +val _ = Context.>> (Context.map_theory CompressData.init);
    23.9  
   23.10  
   23.11  (* compress types *)

    24.1 --- a/src/Pure/context.ML	Fri Mar 28 19:43:54 2008 +0100
    24.2 +++ b/src/Pure/context.ML	Fri Mar 28 20:02:04 2008 +0100
    24.3 @@ -66,8 +66,8 @@
    24.4    val the_thread_data: unit -> generic
    24.5    val set_thread_data: generic option -> unit
    24.6    val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
    24.7 -  val >> : (theory -> theory) -> unit
    24.8 -  val >>> : (theory -> 'a * theory) -> 'a
    24.9 +  val >> : (generic -> generic) -> unit
   24.10 +  val >>> : (generic -> 'a * generic) -> 'a
   24.11  end;
   24.12  
   24.13  signature PRIVATE_CONTEXT =
   24.14 @@ -525,12 +525,12 @@
   24.15  
   24.16  fun >>> f =
   24.17    let
   24.18 -    val (res, thy') = f (the_theory (the_thread_data ()));
   24.19 -    val _ = set_thread_data (SOME (Theory thy'));
   24.20 +    val (res, context') = f (the_thread_data ());
   24.21 +    val _ = set_thread_data (SOME context');
   24.22    in res end;
   24.23  
   24.24  nonfix >>;
   24.25 -fun >> f = >>> (fn thy => ((), f thy));
   24.26 +fun >> f = >>> (fn context => ((), f context));
   24.27  
   24.28  val _ = set_thread_data (SOME (Theory pre_pure_thy));
   24.29  

    25.1 --- a/src/Pure/pure_setup.ML	Fri Mar 28 19:43:54 2008 +0100
    25.2 +++ b/src/Pure/pure_setup.ML	Fri Mar 28 20:02:04 2008 +0100
    25.3 @@ -16,8 +16,9 @@
    25.4  
    25.5  (* the Pure theories *)
    25.6  
    25.7 -Context.>> (OuterSyntax.process_file (Path.explode "Pure.thy"));
    25.8 -Context.>> Theory.end_theory;
    25.9 +Context.>> (Context.map_theory
   25.10 + (OuterSyntax.process_file (Path.explode "Pure.thy") #>
   25.11 +  Theory.end_theory));
   25.12  structure Pure = struct val thy = ML_Context.the_global_context () end;
   25.13  Context.set_thread_data NONE;
   25.14  ThyInfo.register_theory Pure.thy;

    26.1 --- a/src/Pure/pure_thy.ML	Fri Mar 28 19:43:54 2008 +0100
    26.2 +++ b/src/Pure/pure_thy.ML	Fri Mar 28 20:02:04 2008 +0100
    26.3 @@ -146,7 +146,7 @@
    26.4      ref (make_thms NameSpace.empty_table (Facts.merge (all_facts1, all_facts2)));
    26.5  );
    26.6  
    26.7 -val _ = Context.>> TheoremsData.init;
    26.8 +val _ = Context.>> (Context.map_theory TheoremsData.init);
    26.9  
   26.10  val get_theorems_ref = TheoremsData.get;
   26.11  val get_theorems = (fn Thms args => args) o ! o get_theorems_ref;
   26.12 @@ -423,7 +423,7 @@
   26.13  val term = SimpleSyntax.read_term;
   26.14  val prop = SimpleSyntax.read_prop;
   26.15  
   26.16 -val _ = Context.>>
   26.17 +val _ = Context.>> (Context.map_theory
   26.18    (Sign.add_types
   26.19     [("fun", 2, NoSyn),
   26.20      ("prop", 0, NoSyn),
   26.21 @@ -515,7 +515,7 @@
   26.22      ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
   26.23    #> Sign.hide_consts false ["conjunction", "term"]
   26.24    #> add_thmss [(("nothing", []), [])] #> snd
   26.25 -  #> Theory.add_axioms_i Proofterm.equality_axms);
   26.26 +  #> Theory.add_axioms_i Proofterm.equality_axms));
   26.27  
   26.28  end;
   26.29  

    27.1 --- a/src/Pure/simplifier.ML	Fri Mar 28 19:43:54 2008 +0100
    27.2 +++ b/src/Pure/simplifier.ML	Fri Mar 28 20:02:04 2008 +0100
    27.3 @@ -105,7 +105,7 @@
    27.4    fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
    27.5  );
    27.6  
    27.7 -val _ = Context.>> GlobalSimpset.init;
    27.8 +val _ = Context.>> (Context.map_theory GlobalSimpset.init);
    27.9  fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
   27.10  val get_simpset = ! o GlobalSimpset.get;
   27.11  
   27.12 @@ -369,12 +369,12 @@
   27.13  
   27.14  (* setup attributes *)
   27.15  
   27.16 -val _ = Context.>>
   27.17 +val _ = Context.>> (Context.map_theory
   27.18   (Attrib.add_attributes
   27.19     [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
   27.20      (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
   27.21      ("simproc", simproc_att, "declaration of simplification procedures"),
   27.22 -    ("simplified", simplified, "simplified rule")]);
   27.23 +    ("simplified", simplified, "simplified rule")]));
   27.24  
   27.25  
   27.26