tuned;

--- a/src/Pure/ROOT.ML	Wed Oct 22 11:36:43 1997 +0200
+++ b/src/Pure/ROOT.ML	Thu Oct 23 12:09:31 1997 +0200
@@ -48,8 +48,8 @@
 use "goals.ML";
 use "axclass.ML";
 
-structure Pure  = struct val thy = Theory.pure_thy end;
-structure CPure = struct val thy = Theory.cpure_thy end;
+structure Pure  = struct val thy = Theory.pure end;
+structure CPure = struct val thy = Theory.cpure end;
 
 (*Theory parser and loader*)
 cd "Thy";

--- a/src/Pure/data.ML	Wed Oct 22 11:36:43 1997 +0200
+++ b/src/Pure/data.ML	Thu Oct 23 12:09:31 1997 +0200
@@ -75,7 +75,7 @@
   in Data (Symtab.make data) end;
 
 
-fun prep_ext data = merge (data, empty);		(* FIXME !? *)
+fun prep_ext data = merge (data, empty);
 
 fun init (Data tab) kind e ext mrg prt =
   Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab))

--- a/src/Pure/theory.ML	Wed Oct 22 11:36:43 1997 +0200
+++ b/src/Pure/theory.ML	Thu Oct 23 12:09:31 1997 +0200
@@ -18,13 +18,9 @@
       parents: theory list}
   val sign_of           : theory -> Sign.sg
   val syn_of            : theory -> Syntax.syntax
-  val stamps_of_thy     : theory -> string ref list
   val parents_of        : theory -> theory list
   val subthy            : theory * theory -> bool
   val eq_thy            : theory * theory -> bool
-  val proto_pure_thy    : theory
-  val pure_thy          : theory
-  val cpure_thy         : theory
   val cert_axm          : Sign.sg -> string * term -> string * term
   val read_axm          : Sign.sg -> string * string -> string * term
   val inferT_axm        : Sign.sg -> string * term -> string * term
@@ -34,6 +30,9 @@
 signature THEORY =
 sig
   include BASIC_THEORY
+  val proto_pure        : theory
+  val pure              : theory
+  val cpure             : theory
   val thmK		: string
   val oracleK		: string
   (*theory extendsion primitives*)
@@ -79,6 +78,7 @@
     (string -> exn -> unit) -> theory -> theory
   val get_data		: theory -> string -> exn
   val put_data		: string * exn -> theory -> theory
+  val prep_ext		: theory -> theory
   val prep_ext_merge    : theory list -> theory
 end;
 
@@ -104,9 +104,6 @@
 val sign_of = #sign o rep_theory;
 val syn_of = #syn o Sign.rep_sg o sign_of;
 
-(*stamps associated with a theory*)
-val stamps_of_thy = #stamps o Sign.rep_sg o sign_of;
-
 (*return the immediate ancestors*)
 val parents_of = #parents o rep_theory;
 
@@ -121,9 +118,9 @@
 fun make_thy sign axms oras parents =
   Theory {sign = sign, new_axioms = axms, oracles = oras, parents = parents};
 
-val proto_pure_thy = make_thy Sign.proto_pure Symtab.null Symtab.null [];
-val pure_thy = make_thy Sign.pure Symtab.null Symtab.null [proto_pure_thy];
-val cpure_thy = make_thy Sign.cpure Symtab.null Symtab.null [proto_pure_thy];
+val proto_pure = make_thy Sign.proto_pure Symtab.null Symtab.null [];
+val pure = make_thy Sign.pure Symtab.null Symtab.null [proto_pure];
+val cpure = make_thy Sign.cpure Symtab.null Symtab.null [proto_pure];
 
 
 
@@ -189,7 +186,7 @@
 val add_path         = ext_sg Sign.add_path;
 val add_space        = ext_sg Sign.add_space;
 val add_name         = ext_sg Sign.add_name;
-
+val prep_ext         = ext_sg (K Sign.prep_ext) ();
 
 
 (** add axioms **)
@@ -393,6 +390,7 @@
   let
     fun is_union thy = forall (fn t => subthy (t, thy)) thys;
     val is_draft = Sign.is_draft o sign_of;
+    val begin_ext = Sign.add_path "/" o Sign.prep_ext;
 
     fun add_sign (sg, Theory {sign, ...}) =
       Sign.merge (sg, sign) handle TERM (msg, _) => error msg;
@@ -405,10 +403,10 @@
     else
       (case find_first is_union thys of
         Some (Theory {sign, oracles, new_axioms = _, parents = _}) =>
-          make_thy (Sign.make_draft sign) Symtab.null oracles thys
+          make_thy (begin_ext sign) Symtab.null oracles thys
       | None =>
           make_thy
-            (Sign.make_draft (foldl add_sign (Sign.proto_pure, thys)))
+            (begin_ext (foldl add_sign (Sign.proto_pure, thys)))
             Symtab.null
             (Symtab.make (gen_distinct eq_ora (flat (map oracles_of thys)))
               handle Symtab.DUPS names => err_dup_oras names)

--- a/src/Pure/thm.ML	Wed Oct 22 11:36:43 1997 +0200
+++ b/src/Pure/thm.ML	Thu Oct 23 12:09:31 1997 +0200
@@ -87,7 +87,6 @@
                                   shyps: sort list, hyps: cterm list, 
                                   prop: cterm}
   val sign_of_thm       : thm -> Sign.sg
-  val stamps_of_thm     : thm -> string ref list
   val transfer		: theory -> thm -> thm
   val tpairs_of         : thm -> (term * term) list
   val prems_of          : thm -> term list
@@ -411,7 +410,6 @@
 
 
 fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
-val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm;
 
 (*merge signatures of two theorems; raise exception if incompatible*)
 fun merge_thm_sgs
@@ -752,7 +750,7 @@
 (* Definition of the relation =?= *)
 val flexpair_def = fix_shyps [] []
   (Thm{sign_ref= Sign.self_ref Sign.proto_pure, 
-       der = Join(Axiom(pure_thy, "flexpair_def"), []),
+       der = Join(Axiom(Theory.proto_pure, "flexpair_def"), []),
        shyps = [], 
        hyps = [], 
        maxidx = 0,