superceded by Pure.thy and CPure.thy;
authorwenzelm
Thu Apr 21 22:02:06 2005 +0200 (2005-04-21)
changeset 15801d2f5ca3c048d
parent 15800 f2215ed00438
child 15802 fda379c17260
superceded by Pure.thy and CPure.thy;
NEWS
bin/isabelle-process
src/HOL/Bali/DefiniteAssignment.thy
src/HOL/Extraction/Higman.thy
src/HOL/HOL.thy
src/HOL/Transitive_Closure.thy
src/Pure/IsaMakefile
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.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/skip_proof.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/ROOT.ML
src/Pure/Thy/html.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thm_database.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/context.ML
src/Pure/goals.ML
src/Pure/proof_general.ML
src/Pure/pure.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
     1.1 --- a/NEWS	Thu Apr 21 22:00:28 2005 +0200
     1.2 +++ b/NEWS	Thu Apr 21 22:02:06 2005 +0200
     1.3 @@ -189,6 +189,13 @@
     1.4  * Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific
     1.5    selections of theorems in named facts via indices.
     1.6  
     1.7 +* Pure: reorganized bootstrapping of the Pure theories; CPure is now
     1.8 +  derived from Pure, which contains all common declarations already.
     1.9 +  Both theories are defined via plain Isabelle/Isar .thy files.
    1.10 +  INCOMPATIBILITY: elements of CPure (such as the CPure.intro /
    1.11 +  CPure.elim / CPure.dest attributes) now appear in the Pure name
    1.12 +  space; use isatool fixcpure to adapt your theory and ML sources.
    1.13 +
    1.14  
    1.15  *** Document preparation ***
    1.16  
     2.1 --- a/bin/isabelle-process	Thu Apr 21 22:00:28 2005 +0200
     2.2 +++ b/bin/isabelle-process	Thu Apr 21 22:02:06 2005 +0200
     2.3 @@ -1,10 +1,7 @@
     2.4  #!/usr/bin/env bash
     2.5  #
     2.6 -
     2.7  # $Id$
     2.8 -
     2.9  # Author: Markus Wenzel, TU Muenchen
    2.10 -# License: GPL (GNU GENERAL PUBLIC LICENSE)
    2.11  #
    2.12  # Isabelle process startup script.
    2.13  
     3.1 --- a/src/HOL/Bali/DefiniteAssignment.thy	Thu Apr 21 22:00:28 2005 +0200
     3.2 +++ b/src/HOL/Bali/DefiniteAssignment.thy	Thu Apr 21 22:02:06 2005 +0200
     3.3 @@ -1346,7 +1346,7 @@
     3.4                subseteq_B_B': "B \<subseteq> B'" 
     3.5          shows "\<exists> A'. Env \<turnstile> B' \<guillemotright>t\<guillemotright> A'"
     3.6  proof -
     3.7 -  note assigned.select_convs [CPure.intro]
     3.8 +  note assigned.select_convs [Pure.intro]
     3.9    from da  
    3.10    show "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
    3.11    proof (induct) 
     4.1 --- a/src/HOL/Extraction/Higman.thy	Thu Apr 21 22:00:28 2005 +0200
     4.2 +++ b/src/HOL/Extraction/Higman.thy	Thu Apr 21 22:02:06 2005 +0200
     4.3 @@ -20,50 +20,50 @@
     4.4  
     4.5  inductive emb
     4.6  intros
     4.7 -  emb0 [CPure.intro]: "([], bs) \<in> emb"
     4.8 -  emb1 [CPure.intro]: "(as, bs) \<in> emb \<Longrightarrow> (as, b # bs) \<in> emb"
     4.9 -  emb2 [CPure.intro]: "(as, bs) \<in> emb \<Longrightarrow> (a # as, a # bs) \<in> emb"
    4.10 +  emb0 [Pure.intro]: "([], bs) \<in> emb"
    4.11 +  emb1 [Pure.intro]: "(as, bs) \<in> emb \<Longrightarrow> (as, b # bs) \<in> emb"
    4.12 +  emb2 [Pure.intro]: "(as, bs) \<in> emb \<Longrightarrow> (a # as, a # bs) \<in> emb"
    4.13  
    4.14  consts
    4.15    L :: "letter list \<Rightarrow> letter list list set"
    4.16  
    4.17  inductive "L v"
    4.18  intros
    4.19 -  L0 [CPure.intro]: "(w, v) \<in> emb \<Longrightarrow> w # ws \<in> L v"
    4.20 -  L1 [CPure.intro]: "ws \<in> L v \<Longrightarrow> w # ws \<in> L v"
    4.21 +  L0 [Pure.intro]: "(w, v) \<in> emb \<Longrightarrow> w # ws \<in> L v"
    4.22 +  L1 [Pure.intro]: "ws \<in> L v \<Longrightarrow> w # ws \<in> L v"
    4.23  
    4.24  consts
    4.25    good :: "letter list list set"
    4.26  
    4.27  inductive good
    4.28  intros
    4.29 -  good0 [CPure.intro]: "ws \<in> L w \<Longrightarrow> w # ws \<in> good"
    4.30 -  good1 [CPure.intro]: "ws \<in> good \<Longrightarrow> w # ws \<in> good"
    4.31 +  good0 [Pure.intro]: "ws \<in> L w \<Longrightarrow> w # ws \<in> good"
    4.32 +  good1 [Pure.intro]: "ws \<in> good \<Longrightarrow> w # ws \<in> good"
    4.33  
    4.34  consts
    4.35    R :: "letter \<Rightarrow> (letter list list \<times> letter list list) set"
    4.36  
    4.37  inductive "R a"
    4.38  intros
    4.39 -  R0 [CPure.intro]: "([], []) \<in> R a"
    4.40 -  R1 [CPure.intro]: "(vs, ws) \<in> R a \<Longrightarrow> (w # vs, (a # w) # ws) \<in> R a"
    4.41 +  R0 [Pure.intro]: "([], []) \<in> R a"
    4.42 +  R1 [Pure.intro]: "(vs, ws) \<in> R a \<Longrightarrow> (w # vs, (a # w) # ws) \<in> R a"
    4.43  
    4.44  consts
    4.45    T :: "letter \<Rightarrow> (letter list list \<times> letter list list) set"
    4.46  
    4.47  inductive "T a"
    4.48  intros
    4.49 -  T0 [CPure.intro]: "a \<noteq> b \<Longrightarrow> (ws, zs) \<in> R b \<Longrightarrow> (w # zs, (a # w) # zs) \<in> T a"
    4.50 -  T1 [CPure.intro]: "(ws, zs) \<in> T a \<Longrightarrow> (w # ws, (a # w) # zs) \<in> T a"
    4.51 -  T2 [CPure.intro]: "a \<noteq> b \<Longrightarrow> (ws, zs) \<in> T a \<Longrightarrow> (ws, (b # w) # zs) \<in> T a"
    4.52 +  T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> (ws, zs) \<in> R b \<Longrightarrow> (w # zs, (a # w) # zs) \<in> T a"
    4.53 +  T1 [Pure.intro]: "(ws, zs) \<in> T a \<Longrightarrow> (w # ws, (a # w) # zs) \<in> T a"
    4.54 +  T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> (ws, zs) \<in> T a \<Longrightarrow> (ws, (b # w) # zs) \<in> T a"
    4.55  
    4.56  consts
    4.57    bar :: "letter list list set"
    4.58  
    4.59  inductive bar
    4.60  intros
    4.61 -  bar1 [CPure.intro]: "ws \<in> good \<Longrightarrow> ws \<in> bar"
    4.62 -  bar2 [CPure.intro]: "(\<And>w. w # ws \<in> bar) \<Longrightarrow> ws \<in> bar"
    4.63 +  bar1 [Pure.intro]: "ws \<in> good \<Longrightarrow> ws \<in> bar"
    4.64 +  bar2 [Pure.intro]: "(\<And>w. w # ws \<in> bar) \<Longrightarrow> ws \<in> bar"
    4.65  
    4.66  theorem prop1: "([] # ws) \<in> bar" by rules
    4.67  
     5.1 --- a/src/HOL/HOL.thy	Thu Apr 21 22:00:28 2005 +0200
     5.2 +++ b/src/HOL/HOL.thy	Thu Apr 21 22:02:06 2005 +0200
     5.3 @@ -11,28 +11,6 @@
     5.4        ("~~/src/Provers/eqsubst.ML")
     5.5  begin
     5.6  
     5.7 -subsection {* Rules That Belong in Pure *}
     5.8 -
     5.9 -text{*These meta-level elimination rules facilitate the use of assumptions
    5.10 -that contain !! and ==>, especially in linear scripts. *}
    5.11 -
    5.12 -lemma meta_mp:
    5.13 -  assumes major: "PROP P ==> PROP Q" and minor: "PROP P"
    5.14 -  shows "PROP Q"
    5.15 -proof -
    5.16 -  show "PROP Q" by (rule major [OF minor])
    5.17 -qed
    5.18 -
    5.19 -lemma meta_spec:
    5.20 -  assumes major: "!!x. PROP P x"
    5.21 -  shows "PROP P x"
    5.22 -proof -
    5.23 -  show "PROP P x" by (rule major)
    5.24 -qed
    5.25 -
    5.26 -lemmas meta_allE = meta_spec [CPure.elim_format]
    5.27 -
    5.28 -
    5.29  subsection {* Primitive logic *}
    5.30  
    5.31  subsubsection {* Core syntax *}
    5.32 @@ -849,14 +827,14 @@
    5.33    with 1 show R by (rule notE)
    5.34  qed
    5.35  
    5.36 -lemmas [CPure.elim!] = disjE iffE FalseE conjE exE
    5.37 -  and [CPure.intro!] = iffI conjI impI TrueI notI allI refl
    5.38 -  and [CPure.elim 2] = allE notE' impE'
    5.39 -  and [CPure.intro] = exI disjI2 disjI1
    5.40 +lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
    5.41 +  and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
    5.42 +  and [Pure.elim 2] = allE notE' impE'
    5.43 +  and [Pure.intro] = exI disjI2 disjI1
    5.44  
    5.45  lemmas [trans] = trans
    5.46    and [sym] = sym not_sym
    5.47 -  and [CPure.elim?] = iffD1 iffD2 impE
    5.48 +  and [Pure.elim?] = iffD1 iffD2 impE
    5.49  
    5.50  
    5.51  subsubsection {* Atomizing meta-level connectives *}
     6.1 --- a/src/HOL/Transitive_Closure.thy	Thu Apr 21 22:00:28 2005 +0200
     6.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Apr 21 22:02:06 2005 +0200
     6.3 @@ -25,16 +25,16 @@
     6.4  
     6.5  inductive "r^*"
     6.6    intros
     6.7 -    rtrancl_refl [intro!, CPure.intro!, simp]: "(a, a) : r^*"
     6.8 -    rtrancl_into_rtrancl [CPure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
     6.9 +    rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) : r^*"
    6.10 +    rtrancl_into_rtrancl [Pure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
    6.11  
    6.12  consts
    6.13    trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
    6.14  
    6.15  inductive "r^+"
    6.16    intros
    6.17 -    r_into_trancl [intro, CPure.intro]: "(a, b) : r ==> (a, b) : r^+"
    6.18 -    trancl_into_trancl [CPure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
    6.19 +    r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
    6.20 +    trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
    6.21  
    6.22  syntax
    6.23    "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
     7.1 --- a/src/Pure/IsaMakefile	Thu Apr 21 22:00:28 2005 +0200
     7.2 +++ b/src/Pure/IsaMakefile	Thu Apr 21 22:02:06 2005 +0200
     7.3 @@ -23,43 +23,42 @@
     7.4  
     7.5  Pure: $(OUT)/Pure
     7.6  
     7.7 -$(OUT)/Pure: General/ROOT.ML General/buffer.ML General/file.ML		\
     7.8 -  General/graph.ML General/heap.ML General/history.ML			\
     7.9 -  General/lazy_scan.ML General/lazy_seq.ML General/name_space.ML	\
    7.10 -  General/object.ML General/output.ML General/path.ML General/position.ML\
    7.11 -  General/pretty.ML General/scan.ML General/seq.ML General/source.ML	\
    7.12 -  General/susp.ML General/symbol.ML General/table.ML General/url.ML	\
    7.13 -  General/xml.ML\
    7.14 -  IsaPlanner/isaplib.ML  IsaPlanner/term_lib.ML\
    7.15 -  IsaPlanner/isa_fterm.ML IsaPlanner/upterm_lib.ML\
    7.16 -  IsaPlanner/focus_term_lib.ML\
    7.17 -  IsaPlanner/rw_tools.ML IsaPlanner/rw_inst.ML\
    7.18 -  IsaPlanner/isand.ML\
    7.19 -  Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML		\
    7.20 -  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/constdefs.ML\
    7.21 -  Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML		\
    7.22 -  Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML Isar/isar_thy.ML\
    7.23 -  Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML	\
    7.24 -  Isar/obtain.ML Isar/outer_lex.ML Isar/outer_parse.ML			\
    7.25 -  Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML		\
    7.26 -  Isar/proof_data.ML Isar/proof_history.ML Isar/rule_cases.ML		\
    7.27 -  Isar/session.ML Isar/skip_proof.ML Isar/thy_header.ML Isar/toplevel.ML\
    7.28 -  ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML		\
    7.29 -  ML-Systems/polyml.ML ML-Systems/polyml-time-limit.ML			\
    7.30 -  ML-Systems/smlnj-basis-compat.ML ML-Systems/smlnj-compiler.ML		\
    7.31 -  ML-Systems/smlnj-pp-new.ML ML-Systems/smlnj-pp-old.ML			\
    7.32 -  ML-Systems/smlnj.ML Proof/ROOT.ML Proof/extraction.ML			\
    7.33 -  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML Proof/proofchecker.ML\
    7.34 -  Proof/reconstruct.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\
    7.35 -  Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML	\
    7.36 -  Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML\
    7.37 -  Thy/ROOT.ML Thy/html.ML Thy/latex.ML Thy/present.ML Thy/thm_database.ML\
    7.38 -  Thy/thm_deps.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_parse.ML	\
    7.39 -  Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML codegen.ML context.ML display.ML\
    7.40 -  drule.ML envir.ML fact_index.ML goals.ML install_pp.ML library.ML logic.ML\
    7.41 -  meta_simplifier.ML net.ML pattern.ML proof_general.ML proofterm.ML pure.ML\
    7.42 -  pure_thy.ML search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML\
    7.43 -  theory_data.ML thm.ML type.ML type_infer.ML unify.ML
    7.44 +$(OUT)/Pure: General/ROOT.ML General/buffer.ML General/file.ML			\
    7.45 +  General/graph.ML General/heap.ML General/history.ML				\
    7.46 +  General/lazy_scan.ML General/lazy_seq.ML General/name_space.ML		\
    7.47 +  General/object.ML General/output.ML General/path.ML				\
    7.48 +  General/position.ML General/pretty.ML General/scan.ML General/seq.ML		\
    7.49 +  General/source.ML General/susp.ML General/symbol.ML General/table.ML		\
    7.50 +  General/url.ML General/xml.ML IsaPlanner/focus_term_lib.ML			\
    7.51 +  IsaPlanner/isa_fterm.ML IsaPlanner/isand.ML IsaPlanner/isaplib.ML		\
    7.52 +  IsaPlanner/rw_inst.ML IsaPlanner/rw_tools.ML IsaPlanner/term_lib.ML		\
    7.53 +  IsaPlanner/upterm_lib.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML		\
    7.54 +  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/constdefs.ML	\
    7.55 +  Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML			\
    7.56 +  Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML Isar/isar_thy.ML	\
    7.57 +  Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML		\
    7.58 +  Isar/obtain.ML Isar/outer_lex.ML Isar/outer_parse.ML				\
    7.59 +  Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML			\
    7.60 +  Isar/proof_data.ML Isar/proof_history.ML Isar/rule_cases.ML			\
    7.61 +  Isar/session.ML Isar/skip_proof.ML Isar/thy_header.ML Isar/toplevel.ML	\
    7.62 +  ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML			\
    7.63 +  ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML				\
    7.64 +  ML-Systems/smlnj-basis-compat.ML ML-Systems/smlnj-compiler.ML			\
    7.65 +  ML-Systems/smlnj-pp-new.ML ML-Systems/smlnj-pp-old.ML				\
    7.66 +  ML-Systems/smlnj.ML Proof/ROOT.ML Proof/extraction.ML				\
    7.67 +  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML				\
    7.68 +  Proof/proofchecker.ML Proof/reconstruct.ML Pure.thy ROOT.ML			\
    7.69 +  Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML		\
    7.70 +  Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML				\
    7.71 +  Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML			\
    7.72 +  Syntax/type_ext.ML Thy/ROOT.ML Thy/html.ML Thy/latex.ML Thy/present.ML	\
    7.73 +  Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_info.ML Thy/thy_load.ML		\
    7.74 +  Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML codegen.ML		\
    7.75 +  context.ML display.ML drule.ML envir.ML fact_index.ML goals.ML		\
    7.76 +  install_pp.ML library.ML logic.ML meta_simplifier.ML net.ML pattern.ML	\
    7.77 +  proof_general.ML proofterm.ML pure_thy.ML search.ML sign.ML sorts.ML		\
    7.78 +  tactic.ML tctical.ML term.ML theory.ML theory_data.ML thm.ML type.ML		\
    7.79 +  type_infer.ML unify.ML CPure.thy
    7.80  	@./mk
    7.81  
    7.82  
     8.1 --- a/src/Pure/Isar/attrib.ML	Thu Apr 21 22:00:28 2005 +0200
     8.2 +++ b/src/Pure/Isar/attrib.ML	Thu Apr 21 22:02:06 2005 +0200
     8.3 @@ -40,7 +40,6 @@
     8.4    val no_args: 'a attribute -> src -> 'a attribute
     8.5    val add_del_args: 'a attribute -> 'a attribute -> src -> 'a attribute
     8.6    val attribute: (theory attribute * ProofContext.context attribute) -> src
     8.7 -  val setup: (theory -> theory) list
     8.8  end;
     8.9  
    8.10  structure Attrib: ATTRIB =
    8.11 @@ -82,6 +81,7 @@
    8.12  end;
    8.13  
    8.14  structure AttributesData = TheoryDataFun(AttributesDataArgs);
    8.15 +val _ = Context.add_setup [AttributesData.init];
    8.16  val print_attributes = AttributesData.print;
    8.17  
    8.18  
    8.19 @@ -487,15 +487,12 @@
    8.20  fun attribute_global x = (syntax (Scan.lift Args.internal_attribute >> #1)) x;
    8.21  fun attribute_local x = (syntax (Scan.lift Args.internal_attribute >> #2)) x;
    8.22  
    8.23 -val setup_internal_attribute =
    8.24 +val _ = Context.add_setup
    8.25   [PureThy.global_path,
    8.26    add_attributes [(attributeN, (attribute_global, attribute_local), "internal attribute")],
    8.27    PureThy.local_path];
    8.28  
    8.29  
    8.30 -
    8.31 -(** theory setup **)
    8.32 -
    8.33  (* pure_attributes *)
    8.34  
    8.35  val pure_attributes =
    8.36 @@ -522,14 +519,10 @@
    8.37    ("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")] @
    8.38    rule_atts;
    8.39  
    8.40 -
    8.41 -(* setup *)
    8.42 +val _ = Context.add_setup [add_attributes pure_attributes];
    8.43  
    8.44 -val setup =
    8.45 - AttributesData.init :: setup_internal_attribute @ [add_attributes pure_attributes];
    8.46  
    8.47  end;
    8.48  
    8.49  structure BasicAttrib: BASIC_ATTRIB = Attrib;
    8.50  open BasicAttrib;
    8.51 -
     9.1 --- a/src/Pure/Isar/calculation.ML	Thu Apr 21 22:00:28 2005 +0200
     9.2 +++ b/src/Pure/Isar/calculation.ML	Thu Apr 21 22:02:06 2005 +0200
     9.3 @@ -25,7 +25,6 @@
     9.4      -> Proof.state -> Proof.state Seq.seq
     9.5    val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
     9.6    val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
     9.7 -  val setup: (theory -> theory) list
     9.8  end;
     9.9  
    9.10  structure Calculation: CALCULATION =
    9.11 @@ -54,6 +53,7 @@
    9.12  end;
    9.13  
    9.14  structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    9.15 +val _ = Context.add_setup [GlobalCalculation.init];
    9.16  val print_global_rules = GlobalCalculation.print;
    9.17  
    9.18  
    9.19 @@ -69,6 +69,7 @@
    9.20  end;
    9.21  
    9.22  structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
    9.23 +val _ = Context.add_setup [LocalCalculation.init];
    9.24  val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
    9.25  val print_local_rules = LocalCalculation.print;
    9.26  
    9.27 @@ -129,6 +130,16 @@
    9.28   (Attrib.add_del_args sym_add_global sym_del_global,
    9.29    Attrib.add_del_args sym_add_local sym_del_local);
    9.30  
    9.31 +val _ = Context.add_setup
    9.32 + [Attrib.add_attributes
    9.33 +   [("trans", trans_attr, "declaration of transitivity rule"),
    9.34 +    ("sym", sym_attr, "declaration of symmetry rule"),
    9.35 +    ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
    9.36 +      "resolution with symmetry rule")],
    9.37 +  #1 o PureThy.add_thms
    9.38 +   [(("", transitive_thm), [trans_add_global]),
    9.39 +    (("", symmetric_thm), [sym_add_global])]];
    9.40 +
    9.41  
    9.42  
    9.43  (** proof commands **)
    9.44 @@ -207,18 +218,4 @@
    9.45  fun ultimately print = collect true print;
    9.46  
    9.47  
    9.48 -
    9.49 -(** theory setup **)
    9.50 -
    9.51 -val setup =
    9.52 - [GlobalCalculation.init, LocalCalculation.init,
    9.53 -  Attrib.add_attributes
    9.54 -   [("trans", trans_attr, "declaration of transitivity rule"),
    9.55 -    ("sym", sym_attr, "declaration of symmetry rule"),
    9.56 -    ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
    9.57 -      "resolution with symmetry rule")],
    9.58 -  #1 o PureThy.add_thms
    9.59 -   [(("", transitive_thm), [trans_add_global]),
    9.60 -    (("", symmetric_thm), [sym_add_global])]];
    9.61 -
    9.62  end;
    10.1 --- a/src/Pure/Isar/context_rules.ML	Thu Apr 21 22:00:28 2005 +0200
    10.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Apr 21 22:02:06 2005 +0200
    10.3 @@ -49,7 +49,6 @@
    10.4    val addXEs_local: ProofContext.context * thm list -> ProofContext.context
    10.5    val addXDs_local: ProofContext.context * thm list -> ProofContext.context
    10.6    val delrules_local: ProofContext.context * thm list -> ProofContext.context
    10.7 -  val setup: (theory -> theory) list
    10.8  end;
    10.9  
   10.10  structure ContextRules: CONTEXT_RULES =
   10.11 @@ -145,6 +144,7 @@
   10.12  end;
   10.13  
   10.14  structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
   10.15 +val _ = Context.add_setup [GlobalRules.init];
   10.16  val print_global_rules = GlobalRules.print;
   10.17  
   10.18  structure LocalRulesArgs =
   10.19 @@ -156,6 +156,7 @@
   10.20  end;
   10.21  
   10.22  structure LocalRules = ProofDataFun(LocalRulesArgs);
   10.23 +val _ = Context.add_setup [LocalRules.init];
   10.24  val print_local_rules = LocalRules.print;
   10.25  
   10.26  
   10.27 @@ -248,6 +249,9 @@
   10.28  
   10.29  end;
   10.30  
   10.31 +val _ = Context.add_setup
   10.32 +  [#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]];
   10.33 +
   10.34  
   10.35  (* low-level modifiers *)
   10.36  
   10.37 @@ -265,11 +269,4 @@
   10.38  val delrules_local = modifier rule_del_local;
   10.39  
   10.40  
   10.41 -
   10.42 -(** theory setup **)
   10.43 -
   10.44 -val setup =
   10.45 - [GlobalRules.init, LocalRules.init];
   10.46 -
   10.47 -
   10.48  end;
    11.1 --- a/src/Pure/Isar/induct_attrib.ML	Thu Apr 21 22:00:28 2005 +0200
    11.2 +++ b/src/Pure/Isar/induct_attrib.ML	Thu Apr 21 22:02:06 2005 +0200
    11.3 @@ -36,7 +36,6 @@
    11.4    val inductN: string
    11.5    val typeN: string
    11.6    val setN: string
    11.7 -  val setup: (theory -> theory) list
    11.8  end;
    11.9  
   11.10  structure InductAttrib: INDUCT_ATTRIB =
   11.11 @@ -126,6 +125,7 @@
   11.12  end;
   11.13  
   11.14  structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
   11.15 +val _ = Context.add_setup [GlobalInduct.init];
   11.16  val print_global_rules = GlobalInduct.print;
   11.17  val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
   11.18  
   11.19 @@ -142,6 +142,7 @@
   11.20  end;
   11.21  
   11.22  structure LocalInduct = ProofDataFun(LocalInductArgs);
   11.23 +val _ = Context.add_setup [LocalInduct.init];
   11.24  val print_local_rules = LocalInduct.print;
   11.25  val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
   11.26  
   11.27 @@ -223,15 +224,10 @@
   11.28  
   11.29  end;
   11.30  
   11.31 +val _ = Context.add_setup
   11.32 + [Attrib.add_attributes
   11.33 +  [(casesN, cases_attr, "declaration of cases rule for type or set"),
   11.34 +   (inductN, induct_attr, "declaration of induction rule for type or set")]];
   11.35  
   11.36  
   11.37 -(** theory setup **)
   11.38 -
   11.39 -val setup =
   11.40 -  [GlobalInduct.init, LocalInduct.init,
   11.41 -   Attrib.add_attributes
   11.42 -    [(casesN, cases_attr, "declaration of cases rule for type or set"),
   11.43 -     (inductN, induct_attr, "declaration of induction rule for type or set")]];
   11.44 -
   11.45  end;
   11.46 -
    12.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 21 22:00:28 2005 +0200
    12.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 21 22:02:06 2005 +0200
    12.3 @@ -257,7 +257,7 @@
    12.4  
    12.5  val setupP =
    12.6    OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl
    12.7 -    (P.text >> (Toplevel.theory o Context.use_setup));
    12.8 +    (P.text >> (Toplevel.theory o IsarThy.generic_setup));
    12.9  
   12.10  val method_setupP =
   12.11    OuterSyntax.command "method_setup" "define proof method in ML" K.thy_decl
    13.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Apr 21 22:00:28 2005 +0200
    13.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Apr 21 22:02:06 2005 +0200
    13.3 @@ -151,6 +151,7 @@
    13.4    val typed_print_translation: bool * string -> theory -> theory
    13.5    val print_ast_translation: bool * string -> theory -> theory
    13.6    val token_translation: string -> theory -> theory
    13.7 +  val generic_setup: string -> theory -> theory
    13.8    val method_setup: bstring * string * string -> theory -> theory
    13.9    val add_oracle: bstring * string -> theory -> theory
   13.10    val add_locale: bool * bstring * Locale.expr * Locale.element list -> theory -> theory
   13.11 @@ -581,7 +582,13 @@
   13.12      "Theory.add_tokentrfuns token_translation";
   13.13  
   13.14  
   13.15 -(* add method *)
   13.16 +(* generic_setup *)
   13.17 +
   13.18 +val generic_setup =
   13.19 +  Context.use_let "val setup: (theory -> theory) list" "Library.apply setup";
   13.20 +
   13.21 +
   13.22 +(* method_setup *)
   13.23  
   13.24  fun method_setup (name, txt, cmt) =
   13.25    Context.use_let
    14.1 --- a/src/Pure/Isar/locale.ML	Thu Apr 21 22:00:28 2005 +0200
    14.2 +++ b/src/Pure/Isar/locale.ML	Thu Apr 21 22:02:06 2005 +0200
    14.3 @@ -90,9 +90,6 @@
    14.4      string * term list -> thm -> theory -> theory
    14.5    val add_local_witness:
    14.6      string * term list -> thm -> context -> context
    14.7 -
    14.8 -  (* Theory setup for locales *)
    14.9 -  val setup: (theory -> theory) list
   14.10  end;
   14.11  
   14.12  structure Locale: LOCALE =
   14.13 @@ -183,6 +180,9 @@
   14.14  end;
   14.15  
   14.16  structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs);
   14.17 +val _ = Context.add_setup [GlobalLocalesData.init];
   14.18 +
   14.19 +
   14.20  
   14.21  (** context data **)
   14.22  
   14.23 @@ -199,6 +199,7 @@
   14.24  end;
   14.25  
   14.26  structure LocalLocalesData = ProofDataFun(LocalLocalesArgs);
   14.27 +val _ = Context.add_setup [LocalLocalesData.init];
   14.28  
   14.29  
   14.30  (* access locales *)
   14.31 @@ -1882,11 +1883,14 @@
   14.32  in
   14.33  
   14.34  val add_locale = gen_add_locale read_context intern_expr;
   14.35 -
   14.36  val add_locale_i = gen_add_locale cert_context (K I);
   14.37  
   14.38  end;
   14.39  
   14.40 +val _ = Context.add_setup
   14.41 + [add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, SOME Syntax.NoSyn)]],
   14.42 +  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, NONE)]]];
   14.43 +
   14.44  
   14.45  
   14.46  (** Interpretation commands **)
   14.47 @@ -2090,13 +2094,4 @@
   14.48  end;  (* local *)
   14.49  
   14.50  
   14.51 -
   14.52 -(** locale theory setup **)
   14.53 -
   14.54 -val setup =
   14.55 - [GlobalLocalesData.init, LocalLocalesData.init,
   14.56 -  add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, SOME Syntax.NoSyn)]],
   14.57 -  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, NONE)]]];
   14.58 -
   14.59  end;
   14.60 -
    15.1 --- a/src/Pure/Isar/method.ML	Thu Apr 21 22:00:28 2005 +0200
    15.2 +++ b/src/Pure/Isar/method.ML	Thu Apr 21 22:02:06 2005 +0200
    15.3 @@ -115,7 +115,6 @@
    15.4      -> src -> Proof.context -> Proof.method
    15.5    val goal_args_ctxt': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
    15.6      -> (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> Proof.method
    15.7 -  val setup: (theory -> theory) list
    15.8  end;
    15.9  
   15.10  structure Method: METHOD =
   15.11 @@ -529,6 +528,7 @@
   15.12  end;
   15.13  
   15.14  structure MethodsData = TheoryDataFun(MethodsDataArgs);
   15.15 +val _ = Context.add_setup [MethodsData.init];
   15.16  val print_methods = MethodsData.print;
   15.17  
   15.18  
   15.19 @@ -769,9 +769,6 @@
   15.20  val global_done_proof = global_term_proof false (done_text, NONE);
   15.21  
   15.22  
   15.23 -
   15.24 -(** theory setup **)
   15.25 -
   15.26  (* misc tactic emulations *)
   15.27  
   15.28  val subgoal_meth = goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac;
   15.29 @@ -812,17 +809,10 @@
   15.30    ("prolog", thms_args prolog, "simple prolog interpreter"),
   15.31    ("tactic", simple_args Args.name tactic, "ML tactic as proof method")];
   15.32  
   15.33 -
   15.34 -(* setup *)
   15.35 -
   15.36 -val setup =
   15.37 - [MethodsData.init, add_methods pure_methods,
   15.38 -  (#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [ContextRules.intro_query_global NONE])])];
   15.39 +val _ = Context.add_setup [add_methods pure_methods];
   15.40  
   15.41  
   15.42  end;
   15.43  
   15.44 -
   15.45  structure BasicMethod: BASIC_METHOD = Method;
   15.46  open BasicMethod;
   15.47 -
    16.1 --- a/src/Pure/Isar/object_logic.ML	Thu Apr 21 22:00:28 2005 +0200
    16.2 +++ b/src/Pure/Isar/object_logic.ML	Thu Apr 21 22:02:06 2005 +0200
    16.3 @@ -26,7 +26,6 @@
    16.4    val rulify_no_asm: thm -> thm
    16.5    val rule_format: 'a attribute
    16.6    val rule_format_no_asm: 'a attribute
    16.7 -  val setup: (theory -> theory) list
    16.8  end;
    16.9  
   16.10  structure ObjectLogic: OBJECT_LOGIC =
   16.11 @@ -58,6 +57,8 @@
   16.12  end;
   16.13  
   16.14  structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs);
   16.15 +val _ = Context.add_setup [ObjectLogicData.init];
   16.16 +
   16.17  
   16.18  
   16.19  (** generic treatment of judgments -- with a single argument only **)
   16.20 @@ -182,10 +183,4 @@
   16.21  fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
   16.22  
   16.23  
   16.24 -
   16.25 -(** theory setup **)
   16.26 -
   16.27 -val setup = [ObjectLogicData.init];
   16.28 -
   16.29 -
   16.30  end;
    17.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 21 22:00:28 2005 +0200
    17.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 21 22:02:06 2005 +0200
    17.3 @@ -6,6 +6,7 @@
    17.4  *)
    17.5  
    17.6  val show_structs = ref false;
    17.7 +val thms_containing_limit = ref 40;
    17.8  
    17.9  signature PROOF_CONTEXT =
   17.10  sig
   17.11 @@ -153,9 +154,7 @@
   17.12    val prems_limit: int ref
   17.13    val pretty_asms: context -> Pretty.T list
   17.14    val pretty_context: context -> Pretty.T list
   17.15 -  val thms_containing_limit: int ref
   17.16    val print_thms_containing: context -> int option -> string list -> unit
   17.17 -  val setup: (theory -> theory) list
   17.18  end;
   17.19  
   17.20  signature PRIVATE_PROOF_CONTEXT =
   17.21 @@ -268,6 +267,7 @@
   17.22  end;
   17.23  
   17.24  structure ProofDataData = TheoryDataFun(ProofDataDataArgs);
   17.25 +val _ = Context.add_setup [ProofDataData.init];
   17.26  val print_proof_data = ProofDataData.print;
   17.27  
   17.28  
   17.29 @@ -1464,8 +1464,6 @@
   17.30    in gen_distinct eq_fst (List.filter valid (FactIndex.find idx index)) end;
   17.31  
   17.32  
   17.33 -val thms_containing_limit = ref 40;
   17.34 -
   17.35  fun print_thms_containing ctxt opt_limit ss =
   17.36    let
   17.37      val prt_term = pretty_term ctxt;
   17.38 @@ -1499,9 +1497,4 @@
   17.39    end;
   17.40  
   17.41  
   17.42 -
   17.43 -(** theory setup **)
   17.44 -
   17.45 -val setup = [ProofDataData.init];
   17.46 -
   17.47  end;
    18.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Apr 21 22:00:28 2005 +0200
    18.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Apr 21 22:02:06 2005 +0200
    18.3 @@ -15,7 +15,6 @@
    18.4      (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq
    18.5    val global_skip_proof:
    18.6      bool -> Proof.state -> theory * ((string * string) * (string * thm list) list)
    18.7 -  val setup: (theory -> theory) list
    18.8  end;
    18.9  
   18.10  structure SkipProof: SKIP_PROOF =
   18.11 @@ -38,8 +37,8 @@
   18.12    if ! quick_and_dirty then t
   18.13    else error "Proof may be skipped in quick_and_dirty mode only!";
   18.14  
   18.15 -val setup =
   18.16 -  [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path];
   18.17 +val _ = Context.add_setup
   18.18 + [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path];
   18.19  
   18.20  
   18.21  (* basic cheating *)
    19.1 --- a/src/Pure/Proof/extraction.ML	Thu Apr 21 22:00:28 2005 +0200
    19.2 +++ b/src/Pure/Proof/extraction.ML	Thu Apr 21 22:02:06 2005 +0200
    19.3 @@ -25,8 +25,6 @@
    19.4    val mk_typ : typ -> term
    19.5    val etype_of : theory -> string list -> typ list -> term -> typ
    19.6    val realizes_of: theory -> string list -> term -> term -> term
    19.7 -  val parsers: OuterSyntax.parser list
    19.8 -  val setup: (theory -> theory) list
    19.9  end;
   19.10  
   19.11  structure Extraction : EXTRACTION =
   19.12 @@ -226,6 +224,7 @@
   19.13  end;
   19.14  
   19.15  structure ExtractionData = TheoryDataFun(ExtractionArgs);
   19.16 +val _ = Context.add_setup [ExtractionData.init];
   19.17  
   19.18  fun read_condeq thy =
   19.19    let val sg = sign_of (add_syntax thy)
   19.20 @@ -404,6 +403,7 @@
   19.21  
   19.22  fun add_expand_thms thms thy = Library.foldl (fst o add_expand_thm) (thy, thms);
   19.23  
   19.24 +
   19.25  (** types with computational content **)
   19.26  
   19.27  fun add_types tys thy =
   19.28 @@ -417,6 +417,58 @@
   19.29    end;
   19.30  
   19.31  
   19.32 +(** Pure setup **)
   19.33 +
   19.34 +val _ = Context.add_setup
   19.35 +  [add_types [("prop", ([], NONE))],
   19.36 +
   19.37 +   add_typeof_eqns
   19.38 +     ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
   19.39 +    \  (typeof (PROP Q)) == (Type (TYPE('Q))) ==>  \
   19.40 +    \    (typeof (PROP P ==> PROP Q)) == (Type (TYPE('Q)))",
   19.41 +
   19.42 +      "(typeof (PROP Q)) == (Type (TYPE(Null))) ==>  \
   19.43 +    \    (typeof (PROP P ==> PROP Q)) == (Type (TYPE(Null)))",
   19.44 +
   19.45 +      "(typeof (PROP P)) == (Type (TYPE('P))) ==>  \
   19.46 +    \  (typeof (PROP Q)) == (Type (TYPE('Q))) ==>  \
   19.47 +    \    (typeof (PROP P ==> PROP Q)) == (Type (TYPE('P => 'Q)))",
   19.48 +
   19.49 +      "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==>  \
   19.50 +    \    (typeof (!!x. PROP P (x))) == (Type (TYPE(Null)))",
   19.51 +
   19.52 +      "(%x. typeof (PROP P (x))) == (%x. Type (TYPE('P))) ==>  \
   19.53 +    \    (typeof (!!x::'a. PROP P (x))) == (Type (TYPE('a => 'P)))",
   19.54 +
   19.55 +      "(%x. typeof (f (x))) == (%x. Type (TYPE('f))) ==>  \
   19.56 +    \    (typeof (f)) == (Type (TYPE('f)))"],
   19.57 +
   19.58 +   add_realizes_eqns
   19.59 +     ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
   19.60 +    \    (realizes (r) (PROP P ==> PROP Q)) ==  \
   19.61 +    \    (PROP realizes (Null) (PROP P) ==> PROP realizes (r) (PROP Q))",
   19.62 +
   19.63 +      "(typeof (PROP P)) == (Type (TYPE('P))) ==>  \
   19.64 +    \  (typeof (PROP Q)) == (Type (TYPE(Null))) ==>  \
   19.65 +    \    (realizes (r) (PROP P ==> PROP Q)) ==  \
   19.66 +    \    (!!x::'P. PROP realizes (x) (PROP P) ==> PROP realizes (Null) (PROP Q))",
   19.67 +
   19.68 +      "(realizes (r) (PROP P ==> PROP Q)) ==  \
   19.69 +    \  (!!x. PROP realizes (x) (PROP P) ==> PROP realizes (r (x)) (PROP Q))",
   19.70 +
   19.71 +      "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==>  \
   19.72 +    \    (realizes (r) (!!x. PROP P (x))) ==  \
   19.73 +    \    (!!x. PROP realizes (Null) (PROP P (x)))",
   19.74 +
   19.75 +      "(realizes (r) (!!x. PROP P (x))) ==  \
   19.76 +    \  (!!x. PROP realizes (r (x)) (PROP P (x)))"],
   19.77 +
   19.78 +   Attrib.add_attributes
   19.79 +     [("extraction_expand",
   19.80 +       (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute),
   19.81 +       "specify theorems / definitions to be expanded during extraction")]];
   19.82 +
   19.83 +
   19.84  (**** extract program ****)
   19.85  
   19.86  val dummyt = Const ("dummy", dummyT);
   19.87 @@ -753,61 +805,8 @@
   19.88      (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
   19.89        (fn thy => extract (map (apfst (PureThy.get_thm thy o rpair NONE)) xs) thy)));
   19.90  
   19.91 -val parsers = [realizersP, realizabilityP, typeofP, extractP];
   19.92 -
   19.93 -val setup =
   19.94 -  [ExtractionData.init,
   19.95 -
   19.96 -   add_types [("prop", ([], NONE))],
   19.97 -
   19.98 -   add_typeof_eqns
   19.99 -     ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
  19.100 -    \  (typeof (PROP Q)) == (Type (TYPE('Q))) ==>  \
  19.101 -    \    (typeof (PROP P ==> PROP Q)) == (Type (TYPE('Q)))",
  19.102 -
  19.103 -      "(typeof (PROP Q)) == (Type (TYPE(Null))) ==>  \
  19.104 -    \    (typeof (PROP P ==> PROP Q)) == (Type (TYPE(Null)))",
  19.105 -
  19.106 -      "(typeof (PROP P)) == (Type (TYPE('P))) ==>  \
  19.107 -    \  (typeof (PROP Q)) == (Type (TYPE('Q))) ==>  \
  19.108 -    \    (typeof (PROP P ==> PROP Q)) == (Type (TYPE('P => 'Q)))",
  19.109 -
  19.110 -      "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==>  \
  19.111 -    \    (typeof (!!x. PROP P (x))) == (Type (TYPE(Null)))",
  19.112 -
  19.113 -      "(%x. typeof (PROP P (x))) == (%x. Type (TYPE('P))) ==>  \
  19.114 -    \    (typeof (!!x::'a. PROP P (x))) == (Type (TYPE('a => 'P)))",
  19.115 -
  19.116 -      "(%x. typeof (f (x))) == (%x. Type (TYPE('f))) ==>  \
  19.117 -    \    (typeof (f)) == (Type (TYPE('f)))"],
  19.118 -
  19.119 -   add_realizes_eqns
  19.120 -     ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
  19.121 -    \    (realizes (r) (PROP P ==> PROP Q)) ==  \
  19.122 -    \    (PROP realizes (Null) (PROP P) ==> PROP realizes (r) (PROP Q))",
  19.123 -
  19.124 -      "(typeof (PROP P)) == (Type (TYPE('P))) ==>  \
  19.125 -    \  (typeof (PROP Q)) == (Type (TYPE(Null))) ==>  \
  19.126 -    \    (realizes (r) (PROP P ==> PROP Q)) ==  \
  19.127 -    \    (!!x::'P. PROP realizes (x) (PROP P) ==> PROP realizes (Null) (PROP Q))",
  19.128 -
  19.129 -      "(realizes (r) (PROP P ==> PROP Q)) ==  \
  19.130 -    \  (!!x. PROP realizes (x) (PROP P) ==> PROP realizes (r (x)) (PROP Q))",
  19.131 -
  19.132 -      "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==>  \
  19.133 -    \    (realizes (r) (!!x. PROP P (x))) ==  \
  19.134 -    \    (!!x. PROP realizes (Null) (PROP P (x)))",
  19.135 -
  19.136 -      "(realizes (r) (!!x. PROP P (x))) ==  \
  19.137 -    \  (!!x. PROP realizes (r (x)) (PROP P (x)))"],
  19.138 -
  19.139 -   Attrib.add_attributes
  19.140 -     [("extraction_expand",
  19.141 -       (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute),
  19.142 -       "specify theorems / definitions to be expanded during extraction")]];
  19.143 +val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
  19.144  
  19.145  val etype_of = etype_of o sign_of o add_syntax;
  19.146  
  19.147  end;
  19.148 -
  19.149 -OuterSyntax.add_parsers Extraction.parsers;
    20.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Apr 21 22:00:28 2005 +0200
    20.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Apr 21 22:02:06 2005 +0200
    20.3 @@ -12,7 +12,6 @@
    20.4    val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
    20.5    val elim_defs : Sign.sg -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
    20.6    val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
    20.7 -  val setup : (theory -> theory) list
    20.8  end;
    20.9  
   20.10  structure ProofRewriteRules : PROOF_REWRITE_RULES =
   20.11 @@ -182,7 +181,7 @@
   20.12    in rew' end;
   20.13  
   20.14  fun rprocs b = [("Pure/meta_equality", rew b)];
   20.15 -val setup = [Proofterm.add_prf_rprocs (rprocs false)];
   20.16 +val _ = Context.add_setup [Proofterm.add_prf_rprocs (rprocs false)];
   20.17  
   20.18  
   20.19  (**** apply rewriting function to all terms in proof ****)
    21.1 --- a/src/Pure/ROOT.ML	Thu Apr 21 22:00:28 2005 +0200
    21.2 +++ b/src/Pure/ROOT.ML	Thu Apr 21 22:02:06 2005 +0200
    21.3 @@ -63,7 +63,7 @@
    21.4  use "codegen.ML";
    21.5  use "Proof/extraction.ML";
    21.6  
    21.7 -(*old-style goal package*)
    21.8 +(*old goal package -- obsolete*)
    21.9  use "goals.ML";
   21.10  
   21.11  (*the IsaPlanner subsystem*)
   21.12 @@ -72,8 +72,10 @@
   21.13  (*configuration for Proof General*)
   21.14  use "proof_general.ML";
   21.15  
   21.16 -(*final Pure theory setup*)
   21.17 -use "pure.ML";
   21.18 +(*the Pure theories*)
   21.19 +use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;
   21.20 +use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end;
   21.21 +
   21.22  
   21.23  (*several object-logics declare theories that hide basis library structures*)
   21.24  structure BasisLibrary =
    22.1 --- a/src/Pure/Thy/html.ML	Thu Apr 21 22:00:28 2005 +0200
    22.2 +++ b/src/Pure/Thy/html.ML	Thu Apr 21 22:02:06 2005 +0200
    22.3 @@ -38,7 +38,6 @@
    22.4    val section: string -> text
    22.5    val subsection: string -> text
    22.6    val subsubsection: string -> text
    22.7 -  val setup: (theory -> theory) list
    22.8  end;
    22.9  
   22.10  structure HTML: HTML =
   22.11 @@ -254,6 +253,8 @@
   22.12    ("var",   style "var"),
   22.13    ("xstr",  style "xstr")];
   22.14  
   22.15 +val _ = Context.add_setup [Theory.add_mode_tokentrfuns htmlN html_trans];
   22.16 +
   22.17  
   22.18  
   22.19  (** HTML markup **)
   22.20 @@ -427,10 +428,4 @@
   22.21  fun subsubsection heading = "\n\n<h4>" ^ plain heading ^ "</h4>\n";
   22.22  
   22.23  
   22.24 -(** theory setup **)
   22.25 -
   22.26 -val setup =
   22.27 - [Theory.add_mode_tokentrfuns htmlN html_trans];
   22.28 -
   22.29 -
   22.30  end;
    23.1 --- a/src/Pure/Thy/latex.ML	Thu Apr 21 22:00:28 2005 +0200
    23.2 +++ b/src/Pure/Thy/latex.ML	Thu Apr 21 22:02:06 2005 +0200
    23.3 @@ -2,7 +2,7 @@
    23.4      ID:         $Id$
    23.5      Author:     Markus Wenzel, TU Muenchen
    23.6  
    23.7 -LaTeX presentation primitives (based on outer lexical syntax).
    23.8 +LaTeX presentation elements -- based on outer lexical syntax.
    23.9  *)
   23.10  
   23.11  signature LATEX =
    24.1 --- a/src/Pure/Thy/present.ML	Thu Apr 21 22:00:28 2005 +0200
    24.2 +++ b/src/Pure/Thy/present.ML	Thu Apr 21 22:02:06 2005 +0200
    24.3 @@ -34,7 +34,6 @@
    24.4    val subsection: string -> unit
    24.5    val subsubsection: string -> unit
    24.6    val drafts: string -> Path.T list -> Path.T
    24.7 -  val setup: (theory -> theory) list
    24.8  end;
    24.9  
   24.10  structure Present: PRESENT =
   24.11 @@ -86,6 +85,7 @@
   24.12  end;
   24.13  
   24.14  structure BrowserInfoData = TheoryDataFun(BrowserInfoArgs);
   24.15 +val _ = Context.add_setup [BrowserInfoData.init];
   24.16  
   24.17  fun get_info thy =
   24.18    if Theory.eq_thy (thy, ProtoPure.thy) then BrowserInfoArgs.empty
   24.19 @@ -533,11 +533,6 @@
   24.20    in Path.ext doc_format doc_path end;
   24.21  
   24.22  
   24.23 -
   24.24 -(** theory setup **)
   24.25 -
   24.26 -val setup = [BrowserInfoData.init];
   24.27 -
   24.28  end;
   24.29  
   24.30  structure BasicPresent: BASIC_PRESENT = Present;
    25.1 --- a/src/Pure/Thy/thm_database.ML	Thu Apr 21 22:00:28 2005 +0200
    25.2 +++ b/src/Pure/Thy/thm_database.ML	Thu Apr 21 22:02:06 2005 +0200
    25.3 @@ -2,7 +2,7 @@
    25.4      ID:         $Id$
    25.5      Author:     Markus Wenzel, TU Muenchen
    25.6  
    25.7 -Interface to thm database.
    25.8 +Interface to the theorem database.
    25.9  *)
   25.10  
   25.11  signature BASIC_THM_DATABASE =
    26.1 --- a/src/Pure/Thy/thy_info.ML	Thu Apr 21 22:00:28 2005 +0200
    26.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Apr 21 22:02:06 2005 +0200
    26.3 @@ -2,7 +2,8 @@
    26.4      ID:         $Id$
    26.5      Author:     Markus Wenzel, TU Muenchen
    26.6  
    26.7 -Theory loader database, including theory and file dependencies.
    26.8 +Main part of theory loader database, including handling of theory and
    26.9 +file dependencies.
   26.10  *)
   26.11  
   26.12  signature BASIC_THY_INFO =
   26.13 @@ -472,6 +473,8 @@
   26.14      else (change_thys register; perform Update name)
   26.15    end;
   26.16  
   26.17 +val _ = register_theory ProtoPure.thy;
   26.18 +
   26.19  
   26.20  (*final declarations of this structure*)
   26.21  val theory = get_theory;
    27.1 --- a/src/Pure/Thy/thy_load.ML	Thu Apr 21 22:00:28 2005 +0200
    27.2 +++ b/src/Pure/Thy/thy_load.ML	Thu Apr 21 22:02:06 2005 +0200
    27.3 @@ -2,7 +2,7 @@
    27.4      ID:         $Id$
    27.5      Author:     Markus Wenzel, TU Muenchen
    27.6  
    27.7 -Theory loader primitives.
    27.8 +Theory loader primitives, including load path.
    27.9  *)
   27.10  
   27.11  signature BASIC_THY_LOAD =
    28.1 --- a/src/Pure/axclass.ML	Thu Apr 21 22:00:28 2005 +0200
    28.2 +++ b/src/Pure/axclass.ML	Thu Apr 21 22:02:06 2005 +0200
    28.3 @@ -29,10 +29,9 @@
    28.4    val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
    28.5    val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T
    28.6    val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T
    28.7 -  val setup: (theory -> theory) list
    28.8  end;
    28.9  
   28.10 -structure AxClass : AX_CLASS =
   28.11 +structure AxClass: AX_CLASS =
   28.12  struct
   28.13  
   28.14  
   28.15 @@ -192,6 +191,7 @@
   28.16  end;
   28.17  
   28.18  structure AxclassesData = TheoryDataFun(AxclassesArgs);
   28.19 +val _ = Context.add_setup [AxclassesData.init];
   28.20  val print_axclasses = AxclassesData.print;
   28.21  
   28.22  
   28.23 @@ -292,20 +292,13 @@
   28.24    end;
   28.25  
   28.26  
   28.27 -(* intro_classes *)
   28.28 +(* proof methods *)
   28.29  
   28.30  fun intro_classes_tac facts st =
   28.31    (ALLGOALS (Method.insert_tac facts THEN'
   28.32        REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st))))
   28.33      THEN Tactic.distinct_subgoals_tac) st;
   28.34  
   28.35 -val intro_classes_method =
   28.36 -  ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   28.37 -    "back-chain introduction rules of axiomatic type classes");
   28.38 -
   28.39 -
   28.40 -(* default method *)
   28.41 -
   28.42  fun default_intro_classes_tac [] = intro_classes_tac []
   28.43    | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
   28.44  
   28.45 @@ -313,8 +306,10 @@
   28.46    HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   28.47      default_intro_classes_tac facts;
   28.48  
   28.49 -val default_method =
   28.50 -  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule");
   28.51 +val _ = Context.add_setup [Method.add_methods
   28.52 + [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   28.53 +   "back-chain introduction rules of axiomatic type classes"),
   28.54 +  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]];
   28.55  
   28.56  
   28.57  (* old-style axclass_tac *)
   28.58 @@ -419,16 +414,6 @@
   28.59  val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
   28.60  
   28.61  
   28.62 -
   28.63 -(** package setup **)
   28.64 -
   28.65 -(* setup theory *)
   28.66 -
   28.67 -val setup =
   28.68 - [AxclassesData.init,
   28.69 -  Method.add_methods [intro_classes_method, default_method]];
   28.70 -
   28.71 -
   28.72  (* outer syntax *)
   28.73  
   28.74  local structure P = OuterParse and K = OuterSyntax.Keyword in
   28.75 @@ -450,4 +435,3 @@
   28.76  end;
   28.77  
   28.78  end;
   28.79 -
    29.1 --- a/src/Pure/codegen.ML	Thu Apr 21 22:00:28 2005 +0200
    29.2 +++ b/src/Pure/codegen.ML	Thu Apr 21 22:02:06 2005 +0200
    29.3 @@ -55,8 +55,6 @@
    29.4    val test_fn: (int -> (string * term) list option) ref
    29.5    val test_term: theory -> int -> int -> term -> (string * term) list option
    29.6    val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
    29.7 -  val parsers: OuterSyntax.parser list
    29.8 -  val setup: (theory -> theory) list
    29.9  end;
   29.10  
   29.11  structure Codegen : CODEGEN =
   29.12 @@ -169,6 +167,7 @@
   29.13  end;
   29.14  
   29.15  structure CodegenData = TheoryDataFun(CodegenArgs);
   29.16 +val _ = Context.add_setup [CodegenData.init];
   29.17  val print_codegens = CodegenData.print;
   29.18  
   29.19  
   29.20 @@ -228,6 +227,11 @@
   29.21    Attrib.syntax (Scan.peek (fn thy => foldr op || Scan.fail (map mk_parser
   29.22      (#attrs (CodegenData.get thy)))));
   29.23  
   29.24 +val _ = Context.add_setup
   29.25 + [Attrib.add_attributes
   29.26 +  [("code", (code_attr, K Attrib.undef_local_attribute),
   29.27 +     "declare theorems for code generation")]];
   29.28 +
   29.29  
   29.30  (**** preprocessors ****)
   29.31  
   29.32 @@ -254,6 +258,8 @@
   29.33        else th)
   29.34    in (add_preprocessor prep thy, eqn) end;
   29.35  
   29.36 +val _ = Context.add_setup [add_attribute "unfold" (Scan.succeed unfold_attr)];
   29.37 +
   29.38  
   29.39  (**** associate constants with target language code ****)
   29.40  
   29.41 @@ -287,6 +293,7 @@
   29.42  val assoc_consts_i = gen_assoc_consts (K I);
   29.43  val assoc_consts = gen_assoc_consts (fn sg => typ_of o read_ctyp sg);
   29.44  
   29.45 +
   29.46  (**** associate types with target language types ****)
   29.47  
   29.48  fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) =>
   29.49 @@ -553,6 +560,10 @@
   29.50                 (invoke_tycodegen thy dep false) (gr', quotes_of ms)
   29.51             in SOME (gr'', Pretty.block (pretty_mixfix ms ps qs)) end);
   29.52  
   29.53 +val _ = Context.add_setup
   29.54 + [add_codegen "default" default_codegen,
   29.55 +  add_tycodegen "default" default_tycodegen];
   29.56 +
   29.57  
   29.58  fun output_code gr xs = implode (map (snd o Graph.get_node gr)
   29.59    (rev (Graph.all_preds gr xs)));
   29.60 @@ -698,6 +709,10 @@
   29.61       (p, []) => p
   29.62     | _ => error ("Malformed annotation: " ^ quote s));
   29.63  
   29.64 +val _ = Context.add_setup
   29.65 +  [assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")]];
   29.66 +
   29.67 +
   29.68  structure P = OuterParse and K = OuterSyntax.Keyword;
   29.69  
   29.70  val assoc_typeP =
   29.71 @@ -761,18 +776,7 @@
   29.72            (map (fn f => f (Toplevel.sign_of st))) ps, []))
   29.73          (get_test_params (Toplevel.theory_of st), [])) g st)));
   29.74  
   29.75 -val parsers = [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP];
   29.76 -
   29.77 -val setup =
   29.78 -  [CodegenData.init,
   29.79 -   add_codegen "default" default_codegen,
   29.80 -   add_tycodegen "default" default_tycodegen,
   29.81 -   assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")],
   29.82 -   Attrib.add_attributes [("code",
   29.83 -     (code_attr, K Attrib.undef_local_attribute),
   29.84 -     "declare theorems for code generation")],
   29.85 -   add_attribute "unfold" (Scan.succeed unfold_attr)];
   29.86 +val _ = OuterSyntax.add_parsers
   29.87 +  [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP];
   29.88  
   29.89  end;
   29.90 -
   29.91 -OuterSyntax.add_parsers Codegen.parsers;
    30.1 --- a/src/Pure/context.ML	Thu Apr 21 22:00:28 2005 +0200
    30.2 +++ b/src/Pure/context.ML	Thu Apr 21 22:02:06 2005 +0200
    30.3 @@ -2,7 +2,7 @@
    30.4      ID:         $Id$
    30.5      Author:     Markus Wenzel, TU Muenchen
    30.6  
    30.7 -Global theory context.
    30.8 +Theory contexts.
    30.9  *)
   30.10  
   30.11  signature BASIC_CONTEXT =
   30.12 @@ -26,14 +26,15 @@
   30.13    val use_mltext: string -> bool -> theory option -> unit
   30.14    val use_mltext_theory: string -> bool -> theory -> theory
   30.15    val use_let: string -> string -> string -> theory -> theory
   30.16 -  val use_setup: string -> theory -> theory
   30.17 +  val add_setup: (theory -> theory) list -> unit
   30.18 +  val setup: unit -> (theory -> theory) list
   30.19  end;
   30.20  
   30.21  structure Context: CONTEXT =
   30.22  struct
   30.23  
   30.24  
   30.25 -(* theory context *)
   30.26 +(** implicit theory context in ML **)
   30.27  
   30.28  local
   30.29    val current_theory = ref (NONE: theory option);
   30.30 @@ -82,8 +83,16 @@
   30.31  fun use_let bind body txt =
   30.32    use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   30.33  
   30.34 -val use_setup =
   30.35 -  use_let "val setup: (theory -> theory) list" "Library.apply setup";
   30.36 +
   30.37 +
   30.38 +(** delayed theory setup **)
   30.39 +
   30.40 +local
   30.41 +  val setup_fns = ref ([]: (theory -> theory) list);
   30.42 +in
   30.43 +  fun add_setup fns = setup_fns := ! setup_fns @ fns;
   30.44 +  fun setup () = let val fns = ! setup_fns in setup_fns := []; fns end;
   30.45 +end;
   30.46  
   30.47  
   30.48  end;
    31.1 --- a/src/Pure/goals.ML	Thu Apr 21 22:00:28 2005 +0200
    31.2 +++ b/src/Pure/goals.ML	Thu Apr 21 22:02:06 2005 +0200
    31.3 @@ -116,7 +116,6 @@
    31.4    val close_locale: xstring -> theory -> theory
    31.5    val print_scope: theory -> unit
    31.6    val read_cterm: Sign.sg -> string * typ -> cterm
    31.7 -  val setup: (theory -> theory) list
    31.8  end;
    31.9  
   31.10  structure Goals: GOALS =
   31.11 @@ -216,6 +215,7 @@
   31.12  
   31.13  
   31.14  structure LocalesData = TheoryDataFun(LocalesArgs);
   31.15 +val _ = Context.add_setup [LocalesData.init];
   31.16  val print_locales = LocalesData.print;
   31.17  
   31.18  
   31.19 @@ -627,12 +627,6 @@
   31.20      else Sign.pretty_term sign;
   31.21  
   31.22  
   31.23 -(** locale theory setup **)
   31.24 -
   31.25 -val setup =
   31.26 - [LocalesData.init];
   31.27 -
   31.28 -
   31.29  
   31.30  (*** Goal package ***)
   31.31  
    32.1 --- a/src/Pure/proof_general.ML	Thu Apr 21 22:00:28 2005 +0200
    32.2 +++ b/src/Pure/proof_general.ML	Thu Apr 21 22:02:06 2005 +0200
    32.3 @@ -21,7 +21,6 @@
    32.4  
    32.5  signature PROOF_GENERAL =
    32.6  sig
    32.7 -  val setup: (theory -> theory) list
    32.8    val update_thy_only: string -> unit
    32.9    val try_update_thy_only: string -> unit
   32.10    val inform_file_retracted: string -> unit
   32.11 @@ -156,7 +155,11 @@
   32.12     ("bound", tagit bound_tag),
   32.13     ("var", var_or_skolem)];
   32.14  
   32.15 -in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
   32.16 +in
   32.17 +
   32.18 +val _ = Context.add_setup [Theory.add_tokentrfuns proof_general_trans];
   32.19 +
   32.20 +end;
   32.21  
   32.22  
   32.23  (* assembling PGIP packets *)
    33.1 --- a/src/Pure/pure.ML	Thu Apr 21 22:00:28 2005 +0200
    33.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.3 @@ -1,50 +0,0 @@
    33.4 -(*  Title:      Pure/pure.ML
    33.5 -    ID:         $Id$
    33.6 -    Author:     Markus Wenzel, TU Muenchen
    33.7 -
    33.8 -Final setup of the Pure theories.
    33.9 -*)
   33.10 -
   33.11 -local
   33.12 -  val common_setup =
   33.13 -    ProofRewriteRules.setup @
   33.14 -    HTML.setup @
   33.15 -    ObjectLogic.setup @
   33.16 -    ProofContext.setup @
   33.17 -    Locale.setup @
   33.18 -    Attrib.setup @
   33.19 -    ContextRules.setup @
   33.20 -    InductAttrib.setup @
   33.21 -    Method.setup @
   33.22 -    Calculation.setup @
   33.23 -    SkipProof.setup @
   33.24 -    AxClass.setup @
   33.25 -    Present.setup @
   33.26 -    ProofGeneral.setup @
   33.27 -    Codegen.setup @
   33.28 -    Extraction.setup @
   33.29 -    Goals.setup;
   33.30 -in
   33.31 -  structure Pure =
   33.32 -  struct
   33.33 -    val thy =
   33.34 -      PureThy.begin_theory Sign.PureN [ProtoPure.thy]
   33.35 -      |> Theory.add_syntax Syntax.pure_appl_syntax
   33.36 -      |> Library.apply common_setup
   33.37 -      |> PureThy.end_theory;
   33.38 -  end;
   33.39 -
   33.40 -  structure CPure =
   33.41 -  struct
   33.42 -    val thy =
   33.43 -      PureThy.begin_theory Sign.CPureN [ProtoPure.thy]
   33.44 -      |> Theory.add_syntax Syntax.pure_applC_syntax
   33.45 -      |> Library.apply common_setup
   33.46 -      |> Theory.copy
   33.47 -      |> PureThy.end_theory;
   33.48 -  end;
   33.49 -end;
   33.50 -
   33.51 -ThyInfo.register_theory ProtoPure.thy;
   33.52 -ThyInfo.register_theory Pure.thy;
   33.53 -ThyInfo.register_theory CPure.thy;
    34.1 --- a/src/Pure/pure_thy.ML	Thu Apr 21 22:00:28 2005 +0200
    34.2 +++ b/src/Pure/pure_thy.ML	Thu Apr 21 22:02:06 2005 +0200
    34.3 @@ -591,6 +591,7 @@
    34.4      ("dummy", 0, NoSyn)]
    34.5    |> Theory.add_nonterminals Syntax.pure_nonterms
    34.6    |> Theory.add_syntax Syntax.pure_syntax
    34.7 +  |> Theory.add_syntax Syntax.pure_appl_syntax
    34.8    |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
    34.9    |> Theory.add_syntax
   34.10     [("==>", "[prop, prop] => prop", Delimfix "op ==>"),
    35.1 --- a/src/Pure/sign.ML	Thu Apr 21 22:00:28 2005 +0200
    35.2 +++ b/src/Pure/sign.ML	Thu Apr 21 22:02:06 2005 +0200
    35.3 @@ -226,8 +226,10 @@
    35.4  
    35.5  fun rep_sg (Sg (_, args)) = args;
    35.6  
    35.7 -fun stamp_names_of (Sg ({stamps, ...}, _)) = rev (map ! stamps);
    35.8 -fun exists_stamp name (Sg ({stamps, ...}, _)) = exists (equal name o !) stamps;
    35.9 +fun stamps_of (Sg ({stamps, ...}, _)) = stamps;
   35.10 +val stamp_names_of = rev o map ! o stamps_of;
   35.11 +fun exists_stamp name = exists (equal name o !) o stamps_of;
   35.12 +
   35.13  fun pretty_sg sg = Pretty.str_list "{" "}" (stamp_names_of sg);
   35.14  val str_of_sg = Pretty.str_of o pretty_sg;
   35.15  val pprint_sg = Pretty.pprint o pretty_sg;
   35.16 @@ -275,11 +277,11 @@
   35.17    fun eq_sg (sg1 as Sg ({id = id1, ...}, _), sg2 as Sg ({id = id2, ...}, _)) =
   35.18      (check_stale sg1; check_stale sg2; id1 = id2);
   35.19  
   35.20 -  fun subsig (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   35.21 -    eq_sg (sg1, sg2) orelse mem_stamp (hd s1, s2);
   35.22 +  fun subsig (sg1, sg2) =
   35.23 +    eq_sg (sg1, sg2) orelse mem_stamp (hd (stamps_of sg1), stamps_of sg2);
   35.24  
   35.25 -  fun subsig_internal (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   35.26 -    eq_sg (sg1, sg2) orelse subset_stamp (s1, s2);
   35.27 +  fun subsig_internal (sg1, sg2) =
   35.28 +    eq_sg (sg1, sg2) orelse subset_stamp (stamps_of sg1, stamps_of sg2);
   35.29  end;
   35.30  
   35.31  
   35.32 @@ -288,8 +290,8 @@
   35.33  (*test if same theory names are contained in signatures' stamps,
   35.34    i.e. if signatures belong to same theory but not necessarily to the
   35.35    same version of it*)
   35.36 -fun same_sg (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   35.37 -  eq_sg (sg1, sg2) orelse eq_set_string (pairself (map (op !)) (s1, s2));
   35.38 +fun same_sg (sg1, sg2) =
   35.39 +  eq_sg (sg1, sg2) orelse eq_set_string (pairself (map ! o stamps_of) (sg1, sg2));
   35.40  
   35.41  (*test for drafts*)
   35.42  fun is_draft (Sg ({stamps = ref name :: _, ...}, _)) =
   35.43 @@ -1187,9 +1189,8 @@
   35.44    if subsig_internal (sg2, sg1) then sg1
   35.45    else if subsig_internal (sg1, sg2) then sg2
   35.46    else
   35.47 -    if exists_stamp PureN sg1 andalso exists_stamp CPureN sg2 orelse
   35.48 -      exists_stamp CPureN sg1 andalso exists_stamp PureN sg2
   35.49 -    then error "Cannot merge Pure and CPure signatures"
   35.50 +    if exists_stamp CPureN sg1 <> exists_stamp CPureN sg2
   35.51 +    then error "Cannot merge Pure and CPure developments"
   35.52    else
   35.53      let
   35.54        val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)},
   35.55 @@ -1239,4 +1240,3 @@
   35.56  end;
   35.57  
   35.58  end;
   35.59 -