eliminated delayed theory setup
authorwenzelm
Thu Mar 27 15:32:15 2008 +0100 (2008-03-27)
changeset 26435bdce320cd426
parent 26434 d004b791218e
child 26436 dfd6947ab5c2
eliminated delayed theory setup
src/Pure/CPure.thy
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/isar_syn.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/skip_proof.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Pure.thy
src/Pure/Thy/html.ML
src/Pure/Thy/term_style.ML
src/Pure/Tools/isabelle_process.ML
src/Pure/assumption.ML
src/Pure/codegen.ML
src/Pure/context.ML
src/Pure/pure_setup.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/CPure.thy	Thu Mar 27 15:32:12 2008 +0100
     1.2 +++ b/src/Pure/CPure.thy	Thu Mar 27 15:32:15 2008 +0100
     1.3 @@ -8,6 +8,14 @@
     1.4  imports Pure
     1.5  begin
     1.6  
     1.7 -setup  -- {* Some syntax modifications, see ROOT.ML *}
     1.8 +no_syntax
     1.9 +  "_appl" :: "('b => 'a) => args => logic"  ("(1_/(1'(_')))" [1000, 0] 1000)
    1.10 +  "_appl" :: "('b => 'a) => args => aprop"  ("(1_/(1'(_')))" [1000, 0] 1000)
    1.11 +
    1.12 +syntax
    1.13 +  "" :: "'a => cargs"  ("_")
    1.14 +  "_cargs" :: "'a => cargs => cargs"  ("_/ _" [1000, 1000] 1000)
    1.15 +  "_applC" :: "('b => 'a) => cargs => logic"  ("(1_/ _)" [1000, 1000] 999)
    1.16 +  "_applC" :: "('b => 'a) => cargs => aprop"  ("(1_/ _)" [1000, 1000] 999)
    1.17  
    1.18  end
     2.1 --- a/src/Pure/Isar/attrib.ML	Thu Mar 27 15:32:12 2008 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Thu Mar 27 15:32:15 2008 +0100
     2.3 @@ -276,7 +276,7 @@
     2.4  
     2.5  (* theory setup *)
     2.6  
     2.7 -val _ = Context.add_setup
     2.8 +val _ = Context.>>
     2.9   (add_attributes
    2.10     [("attribute", internal_att, "internal attribute"),
    2.11      ("tagged", tagged, "tagged theorem"),
    2.12 @@ -379,7 +379,7 @@
    2.13  
    2.14  (* theory setup *)
    2.15  
    2.16 -val _ = Context.add_setup
    2.17 +val _ = Context.>>
    2.18   (register_config Unify.trace_bound_value #>
    2.19    register_config Unify.search_bound_value #>
    2.20    register_config Unify.trace_simp_value #>
     3.1 --- a/src/Pure/Isar/calculation.ML	Thu Mar 27 15:32:12 2008 +0100
     3.2 +++ b/src/Pure/Isar/calculation.ML	Thu Mar 27 15:32:15 2008 +0100
     3.3 @@ -92,7 +92,7 @@
     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.add_setup
     3.8 +val _ = Context.>>
     3.9   (Attrib.add_attributes
    3.10     [("trans", trans_att, "declaration of transitivity rule"),
    3.11      ("sym", sym_att, "declaration of symmetry rule"),
     4.1 --- a/src/Pure/Isar/class.ML	Thu Mar 27 15:32:12 2008 +0100
     4.2 +++ b/src/Pure/Isar/class.ML	Thu Mar 27 15:32:15 2008 +0100
     4.3 @@ -395,7 +395,7 @@
     4.4    HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
     4.5      default_intro_classes_tac facts;
     4.6  
     4.7 -val _ = Context.add_setup (Method.add_methods
     4.8 +val _ = Context.>> (Method.add_methods
     4.9   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    4.10      "back-chain introduction rules of classes"),
    4.11    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
     5.1 --- a/src/Pure/Isar/code.ML	Thu Mar 27 15:32:12 2008 +0100
     5.2 +++ b/src/Pure/Isar/code.ML	Thu Mar 27 15:32:15 2008 +0100
     5.3 @@ -107,7 +107,7 @@
     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.add_setup (Attrib.add_attributes
     5.8 +    Context.>> (Attrib.add_attributes
     5.9        [("code", code_attr, "declare theorems for code generation")])
    5.10    end;
    5.11  
    5.12 @@ -387,7 +387,7 @@
    5.13      in (exec, ref data) end;
    5.14  );
    5.15  
    5.16 -val _ = Context.add_setup CodeData.init;
    5.17 +val _ = Context.>> CodeData.init;
    5.18  
    5.19  fun thy_data f thy = f ((snd o CodeData.get) thy);
    5.20  
    5.21 @@ -864,7 +864,7 @@
    5.22      (remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
    5.23          (*fully applied in order to get right context for mk_rew!*)
    5.24  
    5.25 -val _ = Context.add_setup
    5.26 +val _ = Context.>>
    5.27    (let
    5.28      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    5.29      fun add_simple_attribute (name, f) =
     6.1 --- a/src/Pure/Isar/context_rules.ML	Thu Mar 27 15:32:12 2008 +0100
     6.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Mar 27 15:32:15 2008 +0100
     6.3 @@ -198,7 +198,7 @@
     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.add_setup
     6.8 +val _ = Context.>>
     6.9    (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
    6.10  
    6.11  
    6.12 @@ -215,6 +215,6 @@
    6.13    ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
    6.14      "remove declaration of intro/elim/dest rule")];
    6.15  
    6.16 -val _ = Context.add_setup (Attrib.add_attributes rule_atts);
    6.17 +val _ = Context.>> (Attrib.add_attributes rule_atts);
    6.18  
    6.19  end;
     7.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 15:32:12 2008 +0100
     7.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 15:32:15 2008 +0100
     7.3 @@ -7,7 +7,7 @@
     7.4  
     7.5  signature ISAR_CMD =
     7.6  sig
     7.7 -  val generic_setup: (string * Position.T) option -> theory -> theory
     7.8 +  val generic_setup: string * Position.T -> theory -> theory
     7.9    val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
    7.10    val parse_translation: bool * (string * Position.T) -> theory -> theory
    7.11    val print_translation: bool * (string * Position.T) -> theory -> theory
    7.12 @@ -134,10 +134,9 @@
    7.13  
    7.14  (* generic_setup *)
    7.15  
    7.16 -fun generic_setup NONE = (fn thy => thy |> Context.setup ())
    7.17 -  | generic_setup (SOME (txt, pos)) =
    7.18 -      ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt
    7.19 -      |> Context.theory_map;
    7.20 +fun generic_setup (txt, pos) =
    7.21 +  ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt
    7.22 +  |> Context.theory_map;
    7.23  
    7.24  
    7.25  (* translation functions *)
     8.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Mar 27 15:32:12 2008 +0100
     8.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 27 15:32:15 2008 +0100
     8.3 @@ -323,7 +323,7 @@
     8.4  
     8.5  val _ =
     8.6    OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
     8.7 -    (Scan.option (P.position P.text) >> (Toplevel.theory o IsarCmd.generic_setup));
     8.8 +    (P.position P.text >> (Toplevel.theory o IsarCmd.generic_setup));
     8.9  
    8.10  val _ =
    8.11    OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
     9.1 --- a/src/Pure/Isar/locale.ML	Thu Mar 27 15:32:12 2008 +0100
     9.2 +++ b/src/Pure/Isar/locale.ML	Thu Mar 27 15:32:15 2008 +0100
     9.3 @@ -2000,7 +2000,7 @@
     9.4  
     9.5  end;
     9.6  
     9.7 -val _ = Context.add_setup
     9.8 +val _ = Context.>>
     9.9   (add_locale_i (SOME "") "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
    9.10    snd #> ProofContext.theory_of #>
    9.11    add_locale_i (SOME "") "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
    9.12 @@ -2041,7 +2041,7 @@
    9.13      Method.intros_tac (wits @ intros) facts st
    9.14    end;
    9.15  
    9.16 -val _ = Context.add_setup (Method.add_methods
    9.17 +val _ = Context.>> (Method.add_methods
    9.18    [("intro_locales",
    9.19      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
    9.20      "back-chain introduction rules of locales without unfolding predicates"),
    10.1 --- a/src/Pure/Isar/method.ML	Thu Mar 27 15:32:12 2008 +0100
    10.2 +++ b/src/Pure/Isar/method.ML	Thu Mar 27 15:32:15 2008 +0100
    10.3 @@ -554,7 +554,7 @@
    10.4  
    10.5  (* theory setup *)
    10.6  
    10.7 -val _ = Context.add_setup (add_methods
    10.8 +val _ = Context.>> (add_methods
    10.9   [("fail", no_args fail, "force failure"),
   10.10    ("succeed", no_args succeed, "succeed"),
   10.11    ("-", no_args insert_facts, "do nothing (insert current facts only)"),
    11.1 --- a/src/Pure/Isar/object_logic.ML	Thu Mar 27 15:32:12 2008 +0100
    11.2 +++ b/src/Pure/Isar/object_logic.ML	Thu Mar 27 15:32:15 2008 +0100
    11.3 @@ -193,7 +193,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.add_setup (add_rulify Drule.norm_hhf_eq);
    11.8 +val _ = Context.>> (add_rulify Drule.norm_hhf_eq);
    11.9  
   11.10  
   11.11  (* atomize *)
    12.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 27 15:32:12 2008 +0100
    12.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 27 15:32:15 2008 +0100
    12.3 @@ -571,7 +571,7 @@
    12.4  fun standard_term_uncheck ctxt =
    12.5    map (contract_abbrevs ctxt);
    12.6  
    12.7 -fun add eq what f = Context.add_setup
    12.8 +fun add eq what f = Context.>>
    12.9    (Context.theory_map (what (fn xs => fn ctxt =>
   12.10      let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end)));
   12.11  
   12.12 @@ -922,7 +922,7 @@
   12.13  
   12.14  in
   12.15  
   12.16 -val _ = Context.add_setup
   12.17 +val _ = Context.>>
   12.18   (Sign.add_syntax
   12.19     [("_context_const", "id => 'a", Delimfix "CONST _"),
   12.20      ("_context_const", "longid => 'a", Delimfix "CONST _"),
    13.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Mar 27 15:32:12 2008 +0100
    13.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Mar 27 15:32:15 2008 +0100
    13.3 @@ -218,7 +218,7 @@
    13.4  
    13.5  (* setup *)
    13.6  
    13.7 -val _ = Context.add_setup (Attrib.add_attributes
    13.8 +val _ = Context.>> (Attrib.add_attributes
    13.9   [("where", where_att, "named instantiation of theorem"),
   13.10    ("of", of_att, "positional instantiation of theorem")]);
   13.11  
   13.12 @@ -367,7 +367,7 @@
   13.13  
   13.14  (* setup *)
   13.15  
   13.16 -val _ = Context.add_setup (Method.add_methods
   13.17 +val _ = Context.>> (Method.add_methods
   13.18   [("rule_tac", inst_args_var res_inst_meth,
   13.19      "apply rule (dynamic instantiation)"),
   13.20    ("erule_tac", inst_args_var eres_inst_meth,
    14.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Mar 27 15:32:12 2008 +0100
    14.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Mar 27 15:32:15 2008 +0100
    14.3 @@ -24,7 +24,7 @@
    14.4    if ! quick_and_dirty then prop
    14.5    else error "Proof may be skipped in quick_and_dirty mode only!";
    14.6  
    14.7 -val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof));
    14.8 +val _ = Context.>> (Theory.add_oracle ("skip_proof", skip_proof));
    14.9  
   14.10  
   14.11  (* basic cheating *)
    15.1 --- a/src/Pure/Proof/extraction.ML	Thu Mar 27 15:32:12 2008 +0100
    15.2 +++ b/src/Pure/Proof/extraction.ML	Thu Mar 27 15:32:15 2008 +0100
    15.3 @@ -395,7 +395,7 @@
    15.4  
    15.5  (** Pure setup **)
    15.6  
    15.7 -val _ = Context.add_setup
    15.8 +val _ = Context.>>
    15.9    (add_types [("prop", ([], NONE))] #>
   15.10  
   15.11     add_typeof_eqns
    16.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Mar 27 15:32:12 2008 +0100
    16.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Mar 27 15:32:15 2008 +0100
    16.3 @@ -187,7 +187,7 @@
    16.4    in rew' end;
    16.5  
    16.6  fun rprocs b = [("Pure/meta_equality", rew b)];
    16.7 -val _ = Context.add_setup (fold Proofterm.add_prf_rproc (rprocs false));
    16.8 +val _ = Context.>> (fold Proofterm.add_prf_rproc (rprocs false));
    16.9  
   16.10  
   16.11  (**** apply rewriting function to all terms in proof ****)
    17.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Mar 27 15:32:12 2008 +0100
    17.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Mar 27 15:32:15 2008 +0100
    17.3 @@ -92,7 +92,7 @@
    17.4  
    17.5  in
    17.6  
    17.7 -val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
    17.8 +val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
    17.9  
   17.10  end;
   17.11  
    18.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 27 15:32:12 2008 +0100
    18.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 27 15:32:15 2008 +0100
    18.3 @@ -105,7 +105,7 @@
    18.4  
    18.5  in
    18.6  
    18.7 -val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
    18.8 +val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
    18.9  
   18.10  end;
   18.11  
    19.1 --- a/src/Pure/Pure.thy	Thu Mar 27 15:32:12 2008 +0100
    19.2 +++ b/src/Pure/Pure.thy	Thu Mar 27 15:32:15 2008 +0100
    19.3 @@ -2,10 +2,7 @@
    19.4      ID:         $Id$
    19.5  *)
    19.6  
    19.7 -section {* The Pure theory *}
    19.8 -
    19.9 -setup  -- {* Common setup of internal components *}
   19.10 -
   19.11 +section {* Further content for the Pure theory *}
   19.12  
   19.13  subsection {* Meta-level connectives in assumptions *}
   19.14  
    20.1 --- a/src/Pure/Thy/html.ML	Thu Mar 27 15:32:12 2008 +0100
    20.2 +++ b/src/Pure/Thy/html.ML	Thu Mar 27 15:32:15 2008 +0100
    20.3 @@ -267,7 +267,7 @@
    20.4    ("var",   var_or_skolem),
    20.5    ("xstr",  style "xstr")];
    20.6  
    20.7 -val _ = Context.add_setup (Sign.add_mode_tokentrfuns htmlN html_trans);
    20.8 +val _ = Context.>> (Sign.add_mode_tokentrfuns htmlN html_trans);
    20.9  
   20.10  
   20.11  
    21.1 --- a/src/Pure/Thy/term_style.ML	Thu Mar 27 15:32:12 2008 +0100
    21.2 +++ b/src/Pure/Thy/term_style.ML	Thu Mar 27 15:32:15 2008 +0100
    21.3 @@ -65,7 +65,7 @@
    21.4        " in propositon: " ^ Syntax.string_of_term ctxt t)
    21.5    end;
    21.6  
    21.7 -val _ = Context.add_setup
    21.8 +val _ = Context.>>
    21.9   (add_style "lhs" (fst oo style_binargs) #>
   21.10    add_style "rhs" (snd oo style_binargs) #>
   21.11    add_style "prem1" (style_parm_premise 1) #>
    22.1 --- a/src/Pure/Tools/isabelle_process.ML	Thu Mar 27 15:32:12 2008 +0100
    22.2 +++ b/src/Pure/Tools/isabelle_process.ML	Thu Mar 27 15:32:15 2008 +0100
    22.3 @@ -160,7 +160,7 @@
    22.4  
    22.5  in
    22.6  
    22.7 -val _ = Context.add_setup (Sign.add_tokentrfuns token_trans);
    22.8 +val _ = Context.>> (Sign.add_tokentrfuns token_trans);
    22.9  
   22.10  end;
   22.11  
    23.1 --- a/src/Pure/assumption.ML	Thu Mar 27 15:32:12 2008 +0100
    23.2 +++ b/src/Pure/assumption.ML	Thu Mar 27 15:32:15 2008 +0100
    23.3 @@ -78,7 +78,7 @@
    23.4  
    23.5  (* named prems -- legacy feature *)
    23.6  
    23.7 -val _ = Context.add_setup
    23.8 +val _ = Context.>>
    23.9    (PureThy.add_thms_dynamic ("prems",
   23.10      fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt));
   23.11  
    24.1 --- a/src/Pure/codegen.ML	Thu Mar 27 15:32:12 2008 +0100
    24.2 +++ b/src/Pure/codegen.ML	Thu Mar 27 15:32:15 2008 +0100
    24.3 @@ -339,7 +339,7 @@
    24.4        end)
    24.5    in add_preprocessor prep end;
    24.6  
    24.7 -val _ = Context.add_setup
    24.8 +val _ = Context.>>
    24.9    (let
   24.10      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   24.11    in
   24.12 @@ -786,7 +786,7 @@
   24.13                   (add_edge (node_id, dep) gr'', p module''))
   24.14             end);
   24.15  
   24.16 -val _ = Context.add_setup
   24.17 +val _ = Context.>>
   24.18   (add_codegen "default" default_codegen #>
   24.19    add_tycodegen "default" default_tycodegen);
   24.20  
   24.21 @@ -1026,7 +1026,7 @@
   24.22      else state
   24.23    end;
   24.24  
   24.25 -val _ = Context.add_setup
   24.26 +val _ = Context.>>
   24.27    (Context.theory_map (Specification.add_theorem_hook test_goal'));
   24.28  
   24.29  
   24.30 @@ -1078,7 +1078,7 @@
   24.31    let val {thy, t, ...} = rep_cterm ct
   24.32    in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
   24.33  
   24.34 -val _ = Context.add_setup
   24.35 +val _ = Context.>>
   24.36    (Theory.add_oracle ("evaluation", evaluation_oracle));
   24.37  
   24.38  
    25.1 --- a/src/Pure/context.ML	Thu Mar 27 15:32:12 2008 +0100
    25.2 +++ b/src/Pure/context.ML	Thu Mar 27 15:32:15 2008 +0100
    25.3 @@ -68,9 +68,6 @@
    25.4    val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
    25.5    val >> : (theory -> theory) -> unit
    25.6    val >>> : (theory -> 'a * theory) -> 'a
    25.7 -  (*delayed setup*)
    25.8 -  val add_setup: (theory -> theory) -> unit
    25.9 -  val setup: unit -> theory -> theory
   25.10  end;
   25.11  
   25.12  signature PRIVATE_CONTEXT =
   25.13 @@ -537,17 +534,6 @@
   25.14  
   25.15  val _ = set_thread_data (SOME (Theory pre_pure_thy));
   25.16  
   25.17 -
   25.18 -
   25.19 -(** delayed theory setup **)
   25.20 -
   25.21 -local
   25.22 -  val setup_fn = ref (I: theory -> theory);
   25.23 -in
   25.24 -  fun add_setup f = CRITICAL (fn () => setup_fn := (! setup_fn #> f));
   25.25 -  fun setup () = CRITICAL (fn () => let val f = ! setup_fn in setup_fn := I; f end);
   25.26 -end;
   25.27 -
   25.28  end;
   25.29  
   25.30  structure BasicContext: BASIC_CONTEXT = Context;
    26.1 --- a/src/Pure/pure_setup.ML	Thu Mar 27 15:32:12 2008 +0100
    26.2 +++ b/src/Pure/pure_setup.ML	Thu Mar 27 15:32:15 2008 +0100
    26.3 @@ -22,9 +22,6 @@
    26.4  Context.set_thread_data NONE;
    26.5  ThyInfo.register_theory Pure.thy;
    26.6  
    26.7 -Context.add_setup
    26.8 - (Sign.del_modesyntax_i Syntax.mode_default PureThy.appl_syntax #>
    26.9 -  Sign.add_syntax_i PureThy.applC_syntax);
   26.10  use_thy "CPure";
   26.11  structure CPure = struct val thy = theory "CPure" end;
   26.12  
    27.1 --- a/src/Pure/simplifier.ML	Thu Mar 27 15:32:12 2008 +0100
    27.2 +++ b/src/Pure/simplifier.ML	Thu Mar 27 15:32:15 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.add_setup GlobalSimpset.init;
    27.8 +val _ = Context.>> 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,7 +369,7 @@
   27.13  
   27.14  (* setup attributes *)
   27.15  
   27.16 -val _ = Context.add_setup
   27.17 +val _ = Context.>>
   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"),