# HG changeset patch
# User wenzelm
# Date 1206730924 -3600
# Node ID 9283b4185fdfe719a88eeecc1b3ca7a7361508fe
# Parent  dac4e2bce00dc9ffac8f8f160ff436e723cf0f8b
Context.>> : operate on Context.generic;

diff -r dac4e2bce00d -r 9283b4185fdf doc-src/IsarImplementation/Thy/integration.thy
--- a/doc-src/IsarImplementation/Thy/integration.thy	Fri Mar 28 19:43:54 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Fri Mar 28 20:02:04 2008 +0100
@@ -241,7 +241,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML the_context: "unit -> theory"} \\
-  @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
+  @{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\
   \end{mldecls}
 
   \begin{description}
@@ -255,13 +255,8 @@
   information immediately, or produce an explicit @{ML_type
   theory_ref} (cf.\ \secref{sec:context-theory}).
 
-  \item @{ML "Context.>>"}~@{text f} applies theory transformation
-  @{text f} to the current theory of the {\ML} toplevel.  In order to
-  work as expected, the theory should be still under construction, and
-  the Isar language element that invoked the {\ML} compiler in the
-  first place should be ready to accept the changed theory value
-  (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
-  Otherwise the theory becomes stale!
+  \item @{ML "Context.>>"}~@{text f} applies context transformation
+  @{text f} to the implicit context of the {\ML} toplevel.
 
   \end{description}
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -276,7 +276,7 @@
 
 (* theory setup *)
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
  (add_attributes
    [("attribute", internal_att, "internal attribute"),
     ("tagged", tagged, "tagged theorem"),
@@ -301,7 +301,7 @@
     ("rule_format", rule_format, "result put into standard rule format"),
     ("rotated", rotated, "rotated theorem premises"),
     ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
-      "declaration of definitional transformations")]);
+      "declaration of definitional transformations")]));
 
 
 
@@ -379,12 +379,12 @@
 
 (* theory setup *)
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
  (register_config Unify.trace_bound_value #>
   register_config Unify.search_bound_value #>
   register_config Unify.trace_simp_value #>
   register_config Unify.trace_types_value #>
-  register_config MetaSimplifier.simp_depth_limit_value);
+  register_config MetaSimplifier.simp_depth_limit_value));
 
 end;
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/calculation.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -92,14 +92,14 @@
 val trans_att = Attrib.add_del_args trans_add trans_del;
 val sym_att = Attrib.add_del_args sym_add sym_del;
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
  (Attrib.add_attributes
    [("trans", trans_att, "declaration of transitivity rule"),
     ("sym", sym_att, "declaration of symmetry rule"),
     ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
   PureThy.add_thms
    [(("", transitive_thm), [trans_add]),
-    (("", symmetric_thm), [sym_add])] #> snd);
+    (("", symmetric_thm), [sym_add])] #> snd));
 
 
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/class.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -140,7 +140,7 @@
 fun mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
     (defs, operations)) =
   ClassData { consts = consts, base_sort = base_sort, inst = inst,
-    morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom, 
+    morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
     defs = defs, operations = operations };
 fun map_class_data f (ClassData { consts, base_sort, inst, morphism,
     assm_intro, of_class, axiom, defs, operations }) =
@@ -304,7 +304,7 @@
       #> map_types subst_typ;
     fun subst_thm defs = Drule.standard' #> instantiate_class #> lift_axiom
       #> MetaSimplifier.rewrite_rule defs;
-    fun morphism thy defs = 
+    fun morphism thy defs =
       Morphism.typ_morphism subst_typ
       $> Morphism.term_morphism (subst_term thy defs)
       $> Morphism.thm_morphism (subst_thm defs);
@@ -395,11 +395,13 @@
   HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
     default_intro_classes_tac facts;
 
-val _ = Context.>> (Method.add_methods
- [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
-    "back-chain introduction rules of classes"),
-  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
-    "apply some intro/elim rule")]);
+val _ = Context.>> (Context.map_theory
+  (Method.add_methods
+   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
+      "back-chain introduction rules of classes"),
+    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
+      "apply some intro/elim rule")]));
+
 
 
 (** classes and class target **)
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/code.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -107,8 +107,9 @@
     val code_attr = Attrib.syntax (Scan.peek (fn context =>
       List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
   in
-    Context.>> (Attrib.add_attributes
-      [("code", code_attr, "declare theorems for code generation")])
+    Context.>> (Context.map_theory
+      (Attrib.add_attributes
+        [("code", code_attr, "declare theorems for code generation")]))
   end;
 
 
@@ -387,7 +388,7 @@
     in (exec, ref data) end;
 );
 
-val _ = Context.>> CodeData.init;
+val _ = Context.>> (Context.map_theory CodeData.init);
 
 fun thy_data f thy = f ((snd o CodeData.get) thy);
 
@@ -864,7 +865,7 @@
     (remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
         (*fully applied in order to get right context for mk_rew!*)
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
   (let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
     fun add_simple_attribute (name, f) =
@@ -877,7 +878,7 @@
     #> add_del_attribute ("func", (add_func, del_func))
     #> add_del_attribute ("inline", (add_inline, del_inline))
     #> add_del_attribute ("post", (add_post, del_post))
-  end);
+  end));
 
 
 (** post- and preprocessing **)
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/context_rules.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -198,8 +198,8 @@
 val elim_query  = rule_add elim_queryK I;
 val dest_query  = rule_add elim_queryK Tactic.make_elim;
 
-val _ = Context.>>
-  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
+val _ = Context.>> (Context.map_theory
+  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]));
 
 
 (* concrete syntax *)
@@ -215,6 +215,6 @@
   ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
     "remove declaration of intro/elim/dest rule")];
 
-val _ = Context.>> (Attrib.add_attributes rule_atts);
+val _ = Context.>> (Context.map_theory (Attrib.add_attributes rule_atts));
 
 end;
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -204,7 +204,8 @@
     \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
     \  val name = " ^ quote name ^ ";\n\
     \  exception Arg of T;\n\
-    \  val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
+    \  val _ = Context.>> (Context.map_theory\n\
+    \    (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\
     \  val thy = ML_Context.the_global_context ();\n\
     \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
     \in\n\
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -2000,11 +2000,11 @@
 
 end;
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
  (add_locale_i (SOME "") "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
   snd #> ProofContext.theory_of #>
   add_locale_i (SOME "") "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
-  snd #> ProofContext.theory_of);
+  snd #> ProofContext.theory_of));
 
 
 
@@ -2041,13 +2041,14 @@
     Method.intros_tac (wits @ intros) facts st
   end;
 
-val _ = Context.>> (Method.add_methods
-  [("intro_locales",
-    Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
-    "back-chain introduction rules of locales without unfolding predicates"),
-   ("unfold_locales",
-    Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
-    "back-chain all introduction rules of locales")]);
+val _ = Context.>> (Context.map_theory
+  (Method.add_methods
+    [("intro_locales",
+      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
+      "back-chain introduction rules of locales without unfolding predicates"),
+     ("unfold_locales",
+      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
+      "back-chain all introduction rules of locales")]));
 
 end;
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/method.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -554,31 +554,33 @@
 
 (* theory setup *)
 
-val _ = Context.>> (add_methods
- [("fail", no_args fail, "force failure"),
-  ("succeed", no_args succeed, "succeed"),
-  ("-", no_args insert_facts, "do nothing (insert current facts only)"),
-  ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
-  ("intro", thms_args intro, "repeatedly apply introduction rules"),
-  ("elim", thms_args elim, "repeatedly apply elimination rules"),
-  ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"),
-  ("fold", thms_ctxt_args fold_meth, "fold definitions"),
-  ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
-    "present local premises as object-level statements"),
-  ("iprover", iprover_meth, "intuitionistic proof search"),
-  ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
-  ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
-  ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
-  ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
-  ("this", no_args this, "apply current facts as rules"),
-  ("fact", thms_ctxt_args fact, "composition by facts from context"),
-  ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
-  ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
-    "rename parameters of goal"),
-  ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
-    "rotate assumptions of goal"),
-  ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"),
-  ("raw_tactic", simple_args (Args.position Args.name) raw_tactic, "ML tactic as raw proof method")]);
+val _ = Context.>> (Context.map_theory
+  (add_methods
+   [("fail", no_args fail, "force failure"),
+    ("succeed", no_args succeed, "succeed"),
+    ("-", no_args insert_facts, "do nothing (insert current facts only)"),
+    ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
+    ("intro", thms_args intro, "repeatedly apply introduction rules"),
+    ("elim", thms_args elim, "repeatedly apply elimination rules"),
+    ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"),
+    ("fold", thms_ctxt_args fold_meth, "fold definitions"),
+    ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
+      "present local premises as object-level statements"),
+    ("iprover", iprover_meth, "intuitionistic proof search"),
+    ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
+    ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
+    ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
+    ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
+    ("this", no_args this, "apply current facts as rules"),
+    ("fact", thms_ctxt_args fact, "composition by facts from context"),
+    ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
+    ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
+      "rename parameters of goal"),
+    ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
+      "rotate assumptions of goal"),
+    ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"),
+    ("raw_tactic", simple_args (Args.position Args.name) raw_tactic,
+      "ML tactic as raw proof method")]));
 
 
 (* outer parser *)
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/object_logic.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -193,7 +193,7 @@
 val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
 val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
 
-val _ = Context.>> (add_rulify Drule.norm_hhf_eq);
+val _ = Context.>> (Context.map_theory (add_rulify Drule.norm_hhf_eq));
 
 
 (* atomize *)
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -571,9 +571,8 @@
 fun standard_term_uncheck ctxt =
   map (contract_abbrevs ctxt);
 
-fun add eq what f = Context.>>
-  (Context.theory_map (what (fn xs => fn ctxt =>
-    let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end)));
+fun add eq what f = Context.>> (what (fn xs => fn ctxt =>
+  let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end));
 
 in
 
@@ -922,14 +921,14 @@
 
 in
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
  (Sign.add_syntax
    [("_context_const", "id => 'a", Delimfix "CONST _"),
     ("_context_const", "longid => 'a", Delimfix "CONST _"),
     ("_context_xconst", "id => 'a", Delimfix "XCONST _"),
     ("_context_xconst", "longid => 'a", Delimfix "XCONST _")] #>
   Sign.add_advanced_trfuns
-    ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], []));
+    ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
 
 end;
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -218,9 +218,10 @@
 
 (* setup *)
 
-val _ = Context.>> (Attrib.add_attributes
- [("where", where_att, "named instantiation of theorem"),
-  ("of", of_att, "positional instantiation of theorem")]);
+val _ = Context.>> (Context.map_theory
+  (Attrib.add_attributes
+   [("where", where_att, "named instantiation of theorem"),
+    ("of", of_att, "positional instantiation of theorem")]));
 
 
 
@@ -367,21 +368,22 @@
 
 (* setup *)
 
-val _ = Context.>> (Method.add_methods
- [("rule_tac", inst_args_var res_inst_meth,
-    "apply rule (dynamic instantiation)"),
-  ("erule_tac", inst_args_var eres_inst_meth,
-    "apply rule in elimination manner (dynamic instantiation)"),
-  ("drule_tac", inst_args_var dres_inst_meth,
-    "apply rule in destruct manner (dynamic instantiation)"),
-  ("frule_tac", inst_args_var forw_inst_meth,
-    "apply rule in forward manner (dynamic instantiation)"),
-  ("cut_tac", inst_args_var cut_inst_meth,
-    "cut rule (dynamic instantiation)"),
-  ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
-    "insert subgoal (dynamic instantiation)"),
-  ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
-    "remove premise (dynamic instantiation)")]);
+val _ = Context.>> (Context.map_theory
+  (Method.add_methods
+   [("rule_tac", inst_args_var res_inst_meth,
+      "apply rule (dynamic instantiation)"),
+    ("erule_tac", inst_args_var eres_inst_meth,
+      "apply rule in elimination manner (dynamic instantiation)"),
+    ("drule_tac", inst_args_var dres_inst_meth,
+      "apply rule in destruct manner (dynamic instantiation)"),
+    ("frule_tac", inst_args_var forw_inst_meth,
+      "apply rule in forward manner (dynamic instantiation)"),
+    ("cut_tac", inst_args_var cut_inst_meth,
+      "cut rule (dynamic instantiation)"),
+    ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
+      "insert subgoal (dynamic instantiation)"),
+    ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
+      "remove premise (dynamic instantiation)")]));
 
 end;
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -24,7 +24,8 @@
   if ! quick_and_dirty then prop
   else error "Proof may be skipped in quick_and_dirty mode only!";
 
-val _ = Context.>> (Theory.add_oracle ("skip_proof", skip_proof));
+val _ = Context.>> (Context.map_theory
+  (Theory.add_oracle ("skip_proof", skip_proof)));
 
 
 (* basic cheating *)
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Proof/extraction.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -395,7 +395,7 @@
 
 (** Pure setup **)
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
   (add_types [("prop", ([], NONE))] #>
 
    add_typeof_eqns
@@ -441,7 +441,7 @@
 
    Attrib.add_attributes
      [("extraction_expand", extraction_expand,
-       "specify theorems / definitions to be expanded during extraction")]);
+       "specify theorems / definitions to be expanded during extraction")]));
 
 
 (**** extract program ****)
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -187,7 +187,7 @@
   in rew' end;
 
 fun rprocs b = [("Pure/meta_equality", rew b)];
-val _ = Context.>> (fold Proofterm.add_prf_rproc (rprocs false));
+val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));
 
 
 (**** apply rewriting function to all terms in proof ****)
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -92,7 +92,7 @@
 
 in
 
-val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
+val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns proof_general_trans));
 
 end;
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -105,7 +105,7 @@
 
 in
 
-val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
+val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns proof_general_trans));
 
 end;
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Thy/html.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -267,7 +267,8 @@
   ("var",   var_or_skolem),
   ("xstr",  style "xstr")];
 
-val _ = Context.>> (Sign.add_mode_tokentrfuns htmlN html_trans);
+val _ = Context.>> (Context.map_theory
+  (Sign.add_mode_tokentrfuns htmlN html_trans));
 
 
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Thy/term_style.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -65,7 +65,7 @@
       " in propositon: " ^ Syntax.string_of_term ctxt t)
   end;
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
  (add_style "lhs" (fst oo style_binargs) #>
   add_style "rhs" (snd oo style_binargs) #>
   add_style "prem1" (style_parm_premise 1) #>
@@ -87,6 +87,6 @@
   add_style "prem17" (style_parm_premise 17) #>
   add_style "prem18" (style_parm_premise 18) #>
   add_style "prem19" (style_parm_premise 19) #>
-  add_style "concl" (K Logic.strip_imp_concl));
+  add_style "concl" (K Logic.strip_imp_concl)));
 
 end;
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -160,7 +160,7 @@
 
 in
 
-val _ = Context.>> (Sign.add_tokentrfuns token_trans);
+val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans));
 
 end;
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/assumption.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -79,8 +79,8 @@
 (* named prems -- legacy feature *)
 
 val _ = Context.>>
-  (PureThy.add_thms_dynamic ("prems",
-    fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt));
+  (Context.map_theory (PureThy.add_thms_dynamic ("prems",
+    fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
 
 
 (* add assumptions *)
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/codegen.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -343,8 +343,8 @@
   (let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   in
-    Code.add_attribute ("unfold", Scan.succeed (mk_attribute
-      (fn thm => add_unfold thm #> Code.add_inline thm)))
+    Context.map_theory (Code.add_attribute ("unfold", Scan.succeed (mk_attribute
+      (fn thm => add_unfold thm #> Code.add_inline thm))))
   end);
 
 
@@ -786,9 +786,9 @@
                  (add_edge (node_id, dep) gr'', p module''))
            end);
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
  (add_codegen "default" default_codegen #>
-  add_tycodegen "default" default_tycodegen);
+  add_tycodegen "default" default_tycodegen));
 
 
 fun mk_tuple [p] = p
@@ -1026,8 +1026,7 @@
     else state
   end;
 
-val _ = Context.>>
-  (Context.theory_map (Specification.add_theorem_hook test_goal'));
+val _ = Context.>> (Specification.add_theorem_hook test_goal');
 
 
 (**** Evaluator for terms ****)
@@ -1078,8 +1077,8 @@
   let val {thy, t, ...} = rep_cterm ct
   in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
 
-val _ = Context.>>
-  (Theory.add_oracle ("evaluation", evaluation_oracle));
+val _ = Context.>> (Context.map_theory
+  (Theory.add_oracle ("evaluation", evaluation_oracle)));
 
 
 (**** Interface ****)
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/compress.ML
--- a/src/Pure/compress.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/compress.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -30,7 +30,7 @@
     ref (Termtab.merge (K true) (terms1, terms2)));
 );
 
-val _ = Context.>> CompressData.init;
+val _ = Context.>> (Context.map_theory CompressData.init);
 
 
 (* compress types *)
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/context.ML
--- a/src/Pure/context.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/context.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -66,8 +66,8 @@
   val the_thread_data: unit -> generic
   val set_thread_data: generic option -> unit
   val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
-  val >> : (theory -> theory) -> unit
-  val >>> : (theory -> 'a * theory) -> 'a
+  val >> : (generic -> generic) -> unit
+  val >>> : (generic -> 'a * generic) -> 'a
 end;
 
 signature PRIVATE_CONTEXT =
@@ -525,12 +525,12 @@
 
 fun >>> f =
   let
-    val (res, thy') = f (the_theory (the_thread_data ()));
-    val _ = set_thread_data (SOME (Theory thy'));
+    val (res, context') = f (the_thread_data ());
+    val _ = set_thread_data (SOME context');
   in res end;
 
 nonfix >>;
-fun >> f = >>> (fn thy => ((), f thy));
+fun >> f = >>> (fn context => ((), f context));
 
 val _ = set_thread_data (SOME (Theory pre_pure_thy));
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/pure_setup.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -16,8 +16,9 @@
 
 (* the Pure theories *)
 
-Context.>> (OuterSyntax.process_file (Path.explode "Pure.thy"));
-Context.>> Theory.end_theory;
+Context.>> (Context.map_theory
+ (OuterSyntax.process_file (Path.explode "Pure.thy") #>
+  Theory.end_theory));
 structure Pure = struct val thy = ML_Context.the_global_context () end;
 Context.set_thread_data NONE;
 ThyInfo.register_theory Pure.thy;
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/pure_thy.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -146,7 +146,7 @@
     ref (make_thms NameSpace.empty_table (Facts.merge (all_facts1, all_facts2)));
 );
 
-val _ = Context.>> TheoremsData.init;
+val _ = Context.>> (Context.map_theory TheoremsData.init);
 
 val get_theorems_ref = TheoremsData.get;
 val get_theorems = (fn Thms args => args) o ! o get_theorems_ref;
@@ -423,7 +423,7 @@
 val term = SimpleSyntax.read_term;
 val prop = SimpleSyntax.read_prop;
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
   (Sign.add_types
    [("fun", 2, NoSyn),
     ("prop", 0, NoSyn),
@@ -515,7 +515,7 @@
     ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
   #> Sign.hide_consts false ["conjunction", "term"]
   #> add_thmss [(("nothing", []), [])] #> snd
-  #> Theory.add_axioms_i Proofterm.equality_axms);
+  #> Theory.add_axioms_i Proofterm.equality_axms));
 
 end;
 
diff -r dac4e2bce00d -r 9283b4185fdf src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/simplifier.ML	Fri Mar 28 20:02:04 2008 +0100
@@ -105,7 +105,7 @@
   fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
 );
 
-val _ = Context.>> GlobalSimpset.init;
+val _ = Context.>> (Context.map_theory GlobalSimpset.init);
 fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
 val get_simpset = ! o GlobalSimpset.get;
 
@@ -369,12 +369,12 @@
 
 (* setup attributes *)
 
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
  (Attrib.add_attributes
    [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
     (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
     ("simproc", simproc_att, "declaration of simplification procedures"),
-    ("simplified", simplified, "simplified rule")]);
+    ("simplified", simplified, "simplified rule")]));