tuned;
authorwenzelm
Thu Oct 23 12:09:31 1997 +0200 (1997-10-23)
changeset 3971b19d38604042
parent 3970 e1843233c694
child 3972 87941982f475
tuned;
src/Pure/ROOT.ML
src/Pure/data.ML
src/Pure/theory.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/ROOT.ML	Wed Oct 22 11:36:43 1997 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Thu Oct 23 12:09:31 1997 +0200
     1.3 @@ -48,8 +48,8 @@
     1.4  use "goals.ML";
     1.5  use "axclass.ML";
     1.6  
     1.7 -structure Pure  = struct val thy = Theory.pure_thy end;
     1.8 -structure CPure = struct val thy = Theory.cpure_thy end;
     1.9 +structure Pure  = struct val thy = Theory.pure end;
    1.10 +structure CPure = struct val thy = Theory.cpure end;
    1.11  
    1.12  (*Theory parser and loader*)
    1.13  cd "Thy";
     2.1 --- a/src/Pure/data.ML	Wed Oct 22 11:36:43 1997 +0200
     2.2 +++ b/src/Pure/data.ML	Thu Oct 23 12:09:31 1997 +0200
     2.3 @@ -75,7 +75,7 @@
     2.4    in Data (Symtab.make data) end;
     2.5  
     2.6  
     2.7 -fun prep_ext data = merge (data, empty);		(* FIXME !? *)
     2.8 +fun prep_ext data = merge (data, empty);
     2.9  
    2.10  fun init (Data tab) kind e ext mrg prt =
    2.11    Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab))
     3.1 --- a/src/Pure/theory.ML	Wed Oct 22 11:36:43 1997 +0200
     3.2 +++ b/src/Pure/theory.ML	Thu Oct 23 12:09:31 1997 +0200
     3.3 @@ -18,13 +18,9 @@
     3.4        parents: theory list}
     3.5    val sign_of           : theory -> Sign.sg
     3.6    val syn_of            : theory -> Syntax.syntax
     3.7 -  val stamps_of_thy     : theory -> string ref list
     3.8    val parents_of        : theory -> theory list
     3.9    val subthy            : theory * theory -> bool
    3.10    val eq_thy            : theory * theory -> bool
    3.11 -  val proto_pure_thy    : theory
    3.12 -  val pure_thy          : theory
    3.13 -  val cpure_thy         : theory
    3.14    val cert_axm          : Sign.sg -> string * term -> string * term
    3.15    val read_axm          : Sign.sg -> string * string -> string * term
    3.16    val inferT_axm        : Sign.sg -> string * term -> string * term
    3.17 @@ -34,6 +30,9 @@
    3.18  signature THEORY =
    3.19  sig
    3.20    include BASIC_THEORY
    3.21 +  val proto_pure        : theory
    3.22 +  val pure              : theory
    3.23 +  val cpure             : theory
    3.24    val thmK		: string
    3.25    val oracleK		: string
    3.26    (*theory extendsion primitives*)
    3.27 @@ -79,6 +78,7 @@
    3.28      (string -> exn -> unit) -> theory -> theory
    3.29    val get_data		: theory -> string -> exn
    3.30    val put_data		: string * exn -> theory -> theory
    3.31 +  val prep_ext		: theory -> theory
    3.32    val prep_ext_merge    : theory list -> theory
    3.33  end;
    3.34  
    3.35 @@ -104,9 +104,6 @@
    3.36  val sign_of = #sign o rep_theory;
    3.37  val syn_of = #syn o Sign.rep_sg o sign_of;
    3.38  
    3.39 -(*stamps associated with a theory*)
    3.40 -val stamps_of_thy = #stamps o Sign.rep_sg o sign_of;
    3.41 -
    3.42  (*return the immediate ancestors*)
    3.43  val parents_of = #parents o rep_theory;
    3.44  
    3.45 @@ -121,9 +118,9 @@
    3.46  fun make_thy sign axms oras parents =
    3.47    Theory {sign = sign, new_axioms = axms, oracles = oras, parents = parents};
    3.48  
    3.49 -val proto_pure_thy = make_thy Sign.proto_pure Symtab.null Symtab.null [];
    3.50 -val pure_thy = make_thy Sign.pure Symtab.null Symtab.null [proto_pure_thy];
    3.51 -val cpure_thy = make_thy Sign.cpure Symtab.null Symtab.null [proto_pure_thy];
    3.52 +val proto_pure = make_thy Sign.proto_pure Symtab.null Symtab.null [];
    3.53 +val pure = make_thy Sign.pure Symtab.null Symtab.null [proto_pure];
    3.54 +val cpure = make_thy Sign.cpure Symtab.null Symtab.null [proto_pure];
    3.55  
    3.56  
    3.57  
    3.58 @@ -189,7 +186,7 @@
    3.59  val add_path         = ext_sg Sign.add_path;
    3.60  val add_space        = ext_sg Sign.add_space;
    3.61  val add_name         = ext_sg Sign.add_name;
    3.62 -
    3.63 +val prep_ext         = ext_sg (K Sign.prep_ext) ();
    3.64  
    3.65  
    3.66  (** add axioms **)
    3.67 @@ -393,6 +390,7 @@
    3.68    let
    3.69      fun is_union thy = forall (fn t => subthy (t, thy)) thys;
    3.70      val is_draft = Sign.is_draft o sign_of;
    3.71 +    val begin_ext = Sign.add_path "/" o Sign.prep_ext;
    3.72  
    3.73      fun add_sign (sg, Theory {sign, ...}) =
    3.74        Sign.merge (sg, sign) handle TERM (msg, _) => error msg;
    3.75 @@ -405,10 +403,10 @@
    3.76      else
    3.77        (case find_first is_union thys of
    3.78          Some (Theory {sign, oracles, new_axioms = _, parents = _}) =>
    3.79 -          make_thy (Sign.make_draft sign) Symtab.null oracles thys
    3.80 +          make_thy (begin_ext sign) Symtab.null oracles thys
    3.81        | None =>
    3.82            make_thy
    3.83 -            (Sign.make_draft (foldl add_sign (Sign.proto_pure, thys)))
    3.84 +            (begin_ext (foldl add_sign (Sign.proto_pure, thys)))
    3.85              Symtab.null
    3.86              (Symtab.make (gen_distinct eq_ora (flat (map oracles_of thys)))
    3.87                handle Symtab.DUPS names => err_dup_oras names)
     4.1 --- a/src/Pure/thm.ML	Wed Oct 22 11:36:43 1997 +0200
     4.2 +++ b/src/Pure/thm.ML	Thu Oct 23 12:09:31 1997 +0200
     4.3 @@ -87,7 +87,6 @@
     4.4                                    shyps: sort list, hyps: cterm list, 
     4.5                                    prop: cterm}
     4.6    val sign_of_thm       : thm -> Sign.sg
     4.7 -  val stamps_of_thm     : thm -> string ref list
     4.8    val transfer		: theory -> thm -> thm
     4.9    val tpairs_of         : thm -> (term * term) list
    4.10    val prems_of          : thm -> term list
    4.11 @@ -411,7 +410,6 @@
    4.12  
    4.13  
    4.14  fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
    4.15 -val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm;
    4.16  
    4.17  (*merge signatures of two theorems; raise exception if incompatible*)
    4.18  fun merge_thm_sgs
    4.19 @@ -752,7 +750,7 @@
    4.20  (* Definition of the relation =?= *)
    4.21  val flexpair_def = fix_shyps [] []
    4.22    (Thm{sign_ref= Sign.self_ref Sign.proto_pure, 
    4.23 -       der = Join(Axiom(pure_thy, "flexpair_def"), []),
    4.24 +       der = Join(Axiom(Theory.proto_pure, "flexpair_def"), []),
    4.25         shyps = [], 
    4.26         hyps = [], 
    4.27         maxidx = 0,