# HG changeset patch
# User wenzelm
# Date 1206628335 -3600
# Node ID bdce320cd426299479af72100d96726b83570970
# Parent  d004b791218ee216c406df745f98970f29e6911d
eliminated delayed theory setup

diff -r d004b791218e -r bdce320cd426 src/Pure/CPure.thy
--- a/src/Pure/CPure.thy	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/CPure.thy	Thu Mar 27 15:32:15 2008 +0100
@@ -8,6 +8,14 @@
 imports Pure
 begin
 
-setup  -- {* Some syntax modifications, see ROOT.ML *}
+no_syntax
+  "_appl" :: "('b => 'a) => args => logic"  ("(1_/(1'(_')))" [1000, 0] 1000)
+  "_appl" :: "('b => 'a) => args => aprop"  ("(1_/(1'(_')))" [1000, 0] 1000)
+
+syntax
+  "" :: "'a => cargs"  ("_")
+  "_cargs" :: "'a => cargs => cargs"  ("_/ _" [1000, 1000] 1000)
+  "_applC" :: "('b => 'a) => cargs => logic"  ("(1_/ _)" [1000, 1000] 999)
+  "_applC" :: "('b => 'a) => cargs => aprop"  ("(1_/ _)" [1000, 1000] 999)
 
 end
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -276,7 +276,7 @@
 
 (* theory setup *)
 
-val _ = Context.add_setup
+val _ = Context.>>
  (add_attributes
    [("attribute", internal_att, "internal attribute"),
     ("tagged", tagged, "tagged theorem"),
@@ -379,7 +379,7 @@
 
 (* theory setup *)
 
-val _ = Context.add_setup
+val _ = Context.>>
  (register_config Unify.trace_bound_value #>
   register_config Unify.search_bound_value #>
   register_config Unify.trace_simp_value #>
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/calculation.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -92,7 +92,7 @@
 val trans_att = Attrib.add_del_args trans_add trans_del;
 val sym_att = Attrib.add_del_args sym_add sym_del;
 
-val _ = Context.add_setup
+val _ = Context.>>
  (Attrib.add_attributes
    [("trans", trans_att, "declaration of transitivity rule"),
     ("sym", sym_att, "declaration of symmetry rule"),
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/class.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -395,7 +395,7 @@
   HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
     default_intro_classes_tac facts;
 
-val _ = Context.add_setup (Method.add_methods
+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),
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/code.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -107,7 +107,7 @@
     val code_attr = Attrib.syntax (Scan.peek (fn context =>
       List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
   in
-    Context.add_setup (Attrib.add_attributes
+    Context.>> (Attrib.add_attributes
       [("code", code_attr, "declare theorems for code generation")])
   end;
 
@@ -387,7 +387,7 @@
     in (exec, ref data) end;
 );
 
-val _ = Context.add_setup CodeData.init;
+val _ = Context.>> CodeData.init;
 
 fun thy_data f thy = f ((snd o CodeData.get) thy);
 
@@ -864,7 +864,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.add_setup
+val _ = Context.>>
   (let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
     fun add_simple_attribute (name, f) =
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/context_rules.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -198,7 +198,7 @@
 val elim_query  = rule_add elim_queryK I;
 val dest_query  = rule_add elim_queryK Tactic.make_elim;
 
-val _ = Context.add_setup
+val _ = Context.>>
   (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
 
 
@@ -215,6 +215,6 @@
   ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
     "remove declaration of intro/elim/dest rule")];
 
-val _ = Context.add_setup (Attrib.add_attributes rule_atts);
+val _ = Context.>> (Attrib.add_attributes rule_atts);
 
 end;
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -7,7 +7,7 @@
 
 signature ISAR_CMD =
 sig
-  val generic_setup: (string * Position.T) option -> theory -> theory
+  val generic_setup: string * Position.T -> theory -> theory
   val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
   val parse_translation: bool * (string * Position.T) -> theory -> theory
   val print_translation: bool * (string * Position.T) -> theory -> theory
@@ -134,10 +134,9 @@
 
 (* generic_setup *)
 
-fun generic_setup NONE = (fn thy => thy |> Context.setup ())
-  | generic_setup (SOME (txt, pos)) =
-      ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt
-      |> Context.theory_map;
+fun generic_setup (txt, pos) =
+  ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt
+  |> Context.theory_map;
 
 
 (* translation functions *)
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -323,7 +323,7 @@
 
 val _ =
   OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
-    (Scan.option (P.position P.text) >> (Toplevel.theory o IsarCmd.generic_setup));
+    (P.position P.text >> (Toplevel.theory o IsarCmd.generic_setup));
 
 val _ =
   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -2000,7 +2000,7 @@
 
 end;
 
-val _ = Context.add_setup
+val _ = Context.>>
  (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)]] #>
@@ -2041,7 +2041,7 @@
     Method.intros_tac (wits @ intros) facts st
   end;
 
-val _ = Context.add_setup (Method.add_methods
+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"),
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/method.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -554,7 +554,7 @@
 
 (* theory setup *)
 
-val _ = Context.add_setup (add_methods
+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)"),
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/object_logic.ML	Thu Mar 27 15:32:15 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_setup (add_rulify Drule.norm_hhf_eq);
+val _ = Context.>> (add_rulify Drule.norm_hhf_eq);
 
 
 (* atomize *)
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -571,7 +571,7 @@
 fun standard_term_uncheck ctxt =
   map (contract_abbrevs ctxt);
 
-fun add eq what f = Context.add_setup
+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)));
 
@@ -922,7 +922,7 @@
 
 in
 
-val _ = Context.add_setup
+val _ = Context.>>
  (Sign.add_syntax
    [("_context_const", "id => 'a", Delimfix "CONST _"),
     ("_context_const", "longid => 'a", Delimfix "CONST _"),
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -218,7 +218,7 @@
 
 (* setup *)
 
-val _ = Context.add_setup (Attrib.add_attributes
+val _ = Context.>> (Attrib.add_attributes
  [("where", where_att, "named instantiation of theorem"),
   ("of", of_att, "positional instantiation of theorem")]);
 
@@ -367,7 +367,7 @@
 
 (* setup *)
 
-val _ = Context.add_setup (Method.add_methods
+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,
diff -r d004b791218e -r bdce320cd426 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -24,7 +24,7 @@
   if ! quick_and_dirty then prop
   else error "Proof may be skipped in quick_and_dirty mode only!";
 
-val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof));
+val _ = Context.>> (Theory.add_oracle ("skip_proof", skip_proof));
 
 
 (* basic cheating *)
diff -r d004b791218e -r bdce320cd426 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Proof/extraction.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -395,7 +395,7 @@
 
 (** Pure setup **)
 
-val _ = Context.add_setup
+val _ = Context.>>
   (add_types [("prop", ([], NONE))] #>
 
    add_typeof_eqns
diff -r d004b791218e -r bdce320cd426 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -187,7 +187,7 @@
   in rew' end;
 
 fun rprocs b = [("Pure/meta_equality", rew b)];
-val _ = Context.add_setup (fold Proofterm.add_prf_rproc (rprocs false));
+val _ = Context.>> (fold Proofterm.add_prf_rproc (rprocs false));
 
 
 (**** apply rewriting function to all terms in proof ****)
diff -r d004b791218e -r bdce320cd426 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -92,7 +92,7 @@
 
 in
 
-val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
+val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
 
 end;
 
diff -r d004b791218e -r bdce320cd426 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -105,7 +105,7 @@
 
 in
 
-val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
+val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
 
 end;
 
diff -r d004b791218e -r bdce320cd426 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Pure.thy	Thu Mar 27 15:32:15 2008 +0100
@@ -2,10 +2,7 @@
     ID:         $Id$
 *)
 
-section {* The Pure theory *}
-
-setup  -- {* Common setup of internal components *}
-
+section {* Further content for the Pure theory *}
 
 subsection {* Meta-level connectives in assumptions *}
 
diff -r d004b791218e -r bdce320cd426 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Thy/html.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -267,7 +267,7 @@
   ("var",   var_or_skolem),
   ("xstr",  style "xstr")];
 
-val _ = Context.add_setup (Sign.add_mode_tokentrfuns htmlN html_trans);
+val _ = Context.>> (Sign.add_mode_tokentrfuns htmlN html_trans);
 
 
 
diff -r d004b791218e -r bdce320cd426 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Thy/term_style.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -65,7 +65,7 @@
       " in propositon: " ^ Syntax.string_of_term ctxt t)
   end;
 
-val _ = Context.add_setup
+val _ = Context.>>
  (add_style "lhs" (fst oo style_binargs) #>
   add_style "rhs" (snd oo style_binargs) #>
   add_style "prem1" (style_parm_premise 1) #>
diff -r d004b791218e -r bdce320cd426 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -160,7 +160,7 @@
 
 in
 
-val _ = Context.add_setup (Sign.add_tokentrfuns token_trans);
+val _ = Context.>> (Sign.add_tokentrfuns token_trans);
 
 end;
 
diff -r d004b791218e -r bdce320cd426 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/assumption.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -78,7 +78,7 @@
 
 (* named prems -- legacy feature *)
 
-val _ = Context.add_setup
+val _ = Context.>>
   (PureThy.add_thms_dynamic ("prems",
     fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt));
 
diff -r d004b791218e -r bdce320cd426 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/codegen.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -339,7 +339,7 @@
       end)
   in add_preprocessor prep end;
 
-val _ = Context.add_setup
+val _ = Context.>>
   (let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   in
@@ -786,7 +786,7 @@
                  (add_edge (node_id, dep) gr'', p module''))
            end);
 
-val _ = Context.add_setup
+val _ = Context.>>
  (add_codegen "default" default_codegen #>
   add_tycodegen "default" default_tycodegen);
 
@@ -1026,7 +1026,7 @@
     else state
   end;
 
-val _ = Context.add_setup
+val _ = Context.>>
   (Context.theory_map (Specification.add_theorem_hook test_goal'));
 
 
@@ -1078,7 +1078,7 @@
   let val {thy, t, ...} = rep_cterm ct
   in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
 
-val _ = Context.add_setup
+val _ = Context.>>
   (Theory.add_oracle ("evaluation", evaluation_oracle));
 
 
diff -r d004b791218e -r bdce320cd426 src/Pure/context.ML
--- a/src/Pure/context.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/context.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -68,9 +68,6 @@
   val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
   val >> : (theory -> theory) -> unit
   val >>> : (theory -> 'a * theory) -> 'a
-  (*delayed setup*)
-  val add_setup: (theory -> theory) -> unit
-  val setup: unit -> theory -> theory
 end;
 
 signature PRIVATE_CONTEXT =
@@ -537,17 +534,6 @@
 
 val _ = set_thread_data (SOME (Theory pre_pure_thy));
 
-
-
-(** delayed theory setup **)
-
-local
-  val setup_fn = ref (I: theory -> theory);
-in
-  fun add_setup f = CRITICAL (fn () => setup_fn := (! setup_fn #> f));
-  fun setup () = CRITICAL (fn () => let val f = ! setup_fn in setup_fn := I; f end);
-end;
-
 end;
 
 structure BasicContext: BASIC_CONTEXT = Context;
diff -r d004b791218e -r bdce320cd426 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/pure_setup.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -22,9 +22,6 @@
 Context.set_thread_data NONE;
 ThyInfo.register_theory Pure.thy;
 
-Context.add_setup
- (Sign.del_modesyntax_i Syntax.mode_default PureThy.appl_syntax #>
-  Sign.add_syntax_i PureThy.applC_syntax);
 use_thy "CPure";
 structure CPure = struct val thy = theory "CPure" end;
 
diff -r d004b791218e -r bdce320cd426 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/simplifier.ML	Thu Mar 27 15:32:15 2008 +0100
@@ -105,7 +105,7 @@
   fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
 );
 
-val _ = Context.add_setup GlobalSimpset.init;
+val _ = Context.>> GlobalSimpset.init;
 fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
 val get_simpset = ! o GlobalSimpset.get;
 
@@ -369,7 +369,7 @@
 
 (* setup attributes *)
 
-val _ = Context.add_setup
+val _ = Context.>>
  (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"),