clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;

--- a/src/Pure/System/build.ML	Tue Jul 24 10:44:36 2012 +0200
+++ b/src/Pure/System/build.ML	Tue Jul 24 10:58:43 2012 +0200
@@ -35,15 +35,12 @@
         end;
 
     val _ =
-      Session.init
-        save
-        false (* FIXME reset!? *)
+      Session.init save false
         (Options.bool options "browser_info") browser_info
         (Options.string options "document")
         (Options.bool options "document_graph")
         (space_explode "," (Options.string options "document_variants"))
-        parent
-        base_name
+        parent base_name
         (true (* FIXME copy document/ files on Scala side!? *),
           Options.string options "document_dump")
         ""

--- a/src/Pure/System/build.scala	Tue Jul 24 10:44:36 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Jul 24 10:58:43 2012 +0200
@@ -116,7 +116,7 @@
 
   private case class Session_Entry(
     name: String,
-    reset: Boolean,
+    this_name: Boolean,
     order: Int,
     path: Option[String],
     parent: Option[String],
@@ -196,7 +196,7 @@
           else
             entry.parent match {
               case Some(parent_name) if queue1.defined(parent_name) =>
-                if (entry.reset) entry.name
+                if (entry.this_name) entry.name
                 else parent_name + "-" + entry.name
               case _ => error("Bad parent session")
             }

--- a/src/ZF/ROOT	Tue Jul 24 10:44:36 2012 +0200
+++ b/src/ZF/ROOT	Tue Jul 24 10:58:43 2012 +0200
@@ -1,4 +1,4 @@
-session ZF! (10) in "." = FOL +
+session ZF! (10) in "." = Pure +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge

--- a/src/ZF/ZF.thy	Tue Jul 24 10:44:36 2012 +0200
+++ b/src/ZF/ZF.thy	Tue Jul 24 10:58:43 2012 +0200
@@ -6,7 +6,7 @@
 header{*Zermelo-Fraenkel Set Theory*}
 
 theory ZF
-imports FOL
+imports "~~/src/FOL/FOL"
 begin
 
 declare [[eta_contract = false]]