Minor cleanup of headers and some speedup of the HOL4 import.

--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/Generate-HOL/GenHOL4Base.thy
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 theory GenHOL4Base = HOL4Compat + HOL4Syntax:;
 
 import_segment "hol4";

--- a/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/Generate-HOL/GenHOL4Prob.thy
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 theory GenHOL4Prob = GenHOL4Real:
 
 import_segment "hol4";

--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/Generate-HOL/GenHOL4Real.thy
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 theory GenHOL4Real = GenHOL4Base:
 
 import_segment "hol4";

--- a/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/Generate-HOL/GenHOL4Vec.thy
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 theory GenHOL4Vec = GenHOL4Base:
 
 import_segment "hol4";

--- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/Generate-HOL/GenHOL4Word32.thy
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 theory GenHOL4Word32 = GenHOL4Base:;
 
 import_segment "hol4";

--- a/src/HOL/Import/Generate-HOL/ROOT.ML	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/Generate-HOL/ROOT.ML	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/Generate-HOL/ROOT.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 with_path ".." use_thy "HOL4Compat";
 with_path ".." use_thy "HOL4Syntax";
 use_thy "GenHOL4Prob";

--- a/src/HOL/Import/HOL/README	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL/README	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,20 @@
+(*  Title:      HOL/Import/HOL/README
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 All the files in this directory (except this README, HOL4.thy, and
 ROOT.ML) are automatically generated.  Edit the files in
-../Generate-HOL, if something needs to be changed.
+../Generate-HOL and run "isatool make HOL-Complex-Generate-HOL" in
+~~/src/HOL, if something needs to be changed.
+
+To build the logic in this directory, simply do a "isatool make
+HOL-Import-HOL" in ~~/src/HOL.
+
+Note that the quick_and_dirty flag is on as default for this
+directory, which means that the original HOL4 proofs are not consulted
+at all.  If a real replay of the HOL4 proofs is desired, get and
+unpack the HOL4 proof objects to somewhere on your harddisk, and set
+the variable PROOF_DIRS to the directory where the directory "hol4"
+is.  Now edit the ROOT.ML file to unset the quick_and_dirty flag and
+do "isatool make HOL-Import-HOL" in ~~/src/HOL.

--- a/src/HOL/Import/HOL/ROOT.ML	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/HOL/ROOT.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 with_path ".." use_thy "HOL4Compat";
 with_path ".." use_thy "HOL4Syntax";
 setmp quick_and_dirty true use_thy "HOL4Prob";

--- a/src/HOL/Import/HOL/real.imp	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL/real.imp	Sat Apr 17 23:53:35 2004 +0200
@@ -77,13 +77,13 @@
   "REAL_SUB_RZERO" > "Ring_and_Field.diff_0_right"
   "REAL_SUB_RNEG" > "Ring_and_Field.diff_minus_eq_add"
   "REAL_SUB_REFL" > "Ring_and_Field.diff_self"
-  "REAL_SUB_RDISTRIB" > "Ring_and_Field.left_diff_distrib"
+  "REAL_SUB_RDISTRIB" > "Ring_and_Field.ring_eq_simps_6"
   "REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2"
   "REAL_SUB_LZERO" > "Ring_and_Field.diff_0"
   "REAL_SUB_LT" > "RealDef.real_0_less_diff_iff"
   "REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG"
   "REAL_SUB_LE" > "RealDef.real_0_le_diff_iff"
-  "REAL_SUB_LDISTRIB" > "Ring_and_Field.right_diff_distrib"
+  "REAL_SUB_LDISTRIB" > "Ring_and_Field.ring_eq_simps_7"
   "REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2"
   "REAL_SUB_ADD2" > "Ring_and_Field.add_minus_self_left"
   "REAL_SUB_ADD" > "Ring_and_Field.minus_add_self"
@@ -91,7 +91,7 @@
   "REAL_SUB_0" > "Ring_and_Field.eq_iff_diff_eq_0"
   "REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff"
   "REAL_RINV_UNIQ" > "RealDef.real_inverse_unique"
-  "REAL_RDISTRIB" > "Ring_and_Field.ring_distrib_2"
+  "REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4"
   "REAL_POW_POW" > "Power.power_mult"
   "REAL_POW_MONO_LT" > "Power.power_strict_increasing"
   "REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2"
@@ -129,7 +129,7 @@
   "REAL_NEG_ADD" > "Ring_and_Field.minus_add_distrib"
   "REAL_NEG_0" > "Ring_and_Field.minus_zero"
   "REAL_NEGNEG" > "Ring_and_Field.minus_minus"
-  "REAL_MUL_SYM" > "Ring_and_Field.mult_ac_2"
+  "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2"
   "REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right"
   "REAL_MUL_RNEG" > "Ring_and_Field.minus_mult_right"
   "REAL_MUL_RINV" > "Ring_and_Field.right_inverse"
@@ -243,7 +243,7 @@
   "REAL_LET_ADD" > "HOL4Real.real.REAL_LET_ADD"
   "REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2"
   "REAL_LE" > "RealDef.real_of_nat_le_iff"
-  "REAL_LDISTRIB" > "Ring_and_Field.ring_distrib_1"
+  "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
   "REAL_INV_POS" > "Ring_and_Field.positive_imp_inverse_positive"
   "REAL_INV_NZ" > "Ring_and_Field.nonzero_imp_inverse_nonzero"
   "REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
@@ -257,8 +257,8 @@
   "REAL_INJ" > "RealDef.real_of_nat_inject"
   "REAL_HALF_DOUBLE" > "RComplete.real_sum_of_halves"
   "REAL_FACT_NZ" > "HOL4Real.real.REAL_FACT_NZ"
-  "REAL_EQ_SUB_RADD" > "Ring_and_Field.compare_rls_10"
-  "REAL_EQ_SUB_LADD" > "Ring_and_Field.compare_rls_11"
+  "REAL_EQ_SUB_RADD" > "Ring_and_Field.ring_eq_simps_15"
+  "REAL_EQ_SUB_LADD" > "Ring_and_Field.ring_eq_simps_16"
   "REAL_EQ_RMUL_IMP" > "Ring_and_Field.field_mult_cancel_right_lemma"
   "REAL_EQ_RMUL" > "Ring_and_Field.field_mult_cancel_right"
   "REAL_EQ_RDIV_EQ" > "HOL4Real.real.REAL_EQ_RDIV_EQ"
@@ -283,17 +283,17 @@
   "REAL_DIFFSQ" > "HOL4Real.real.REAL_DIFFSQ"
   "REAL_ARCH_LEAST" > "HOL4Real.real.REAL_ARCH_LEAST"
   "REAL_ARCH" > "RComplete.reals_Archimedean3"
-  "REAL_ADD_SYM" > "Ring_and_Field.add_ac_2"
+  "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9"
   "REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2"
   "REAL_ADD_SUB" > "Ring_and_Field.add_minus_self_right"
   "REAL_ADD_RINV" > "Ring_and_Field.right_minus"
   "REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ"
   "REAL_ADD_RID" > "Ring_and_Field.add_0_right"
-  "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_distrib_2"
+  "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4"
   "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
   "REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ"
   "REAL_ADD_LID" > "Ring_and_Field.abelian_semigroup.add_0"
-  "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_distrib_1"
+  "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
   "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
   "REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2"
   "REAL_ADD" > "RealDef.real_of_nat_add"

--- a/src/HOL/Import/HOL/realax.imp	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL/realax.imp	Sat Apr 17 23:53:35 2004 +0200
@@ -91,7 +91,7 @@
   "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC"
   "TREAL_10" > "HOL4Real.realax.TREAL_10"
   "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
-  "REAL_MUL_SYM" > "Ring_and_Field.mult_ac_2"
+  "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2"
   "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
   "REAL_MUL_LID" > "Ring_and_Field.almost_semiring.mult_1"
   "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
@@ -100,9 +100,9 @@
   "REAL_LT_REFL" > "HOL.order_less_irrefl"
   "REAL_LT_MUL" > "Ring_and_Field.mult_pos"
   "REAL_LT_IADD" > "Ring_and_Field.add_strict_left_mono"
-  "REAL_LDISTRIB" > "Ring_and_Field.ring_distrib_1"
+  "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
   "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero"
-  "REAL_ADD_SYM" > "Ring_and_Field.add_ac_2"
+  "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9"
   "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
   "REAL_ADD_LID" > "Ring_and_Field.abelian_semigroup.add_0"
   "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"

--- a/src/HOL/Import/HOL4Compat.thy	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/HOL4Compat.thy
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 theory HOL4Compat = HOL4Setup + Divides + Primes + Real:
 
 lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"

--- a/src/HOL/Import/HOL4Setup.thy	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL4Setup.thy	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/HOL4Setup.thy
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 theory HOL4Setup = MakeEqual
   files ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML"):
 

--- a/src/HOL/Import/HOL4Syntax.thy	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL4Syntax.thy	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/HOL4Syntax.thy
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 theory HOL4Syntax = HOL4Setup
   files "import_syntax.ML":
 

--- a/src/HOL/Import/MakeEqual.thy	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/MakeEqual.thy	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/MakeEqual.thy
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 theory MakeEqual = Main
   files "shuffler.ML":
 

--- a/src/HOL/Import/ROOT.ML	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/ROOT.ML	Sat Apr 17 23:53:35 2004 +0200
@@ -1,2 +1,7 @@
+(*  Title:      HOL/Import/ROOT.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 use_thy "HOL4Compat";
 use_thy "HOL4Syntax";

--- a/src/HOL/Import/hol4rews.ML	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/hol4rews.ML	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/hol4rews.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord);
 
 type holthm = (term * term) list * thm
@@ -24,7 +29,7 @@
 
 structure ImportSegmentArgs: THEORY_DATA_ARGS =
 struct
-val name = "HOL4/import"
+val name = "HOL4/import_segment"
 type T = string
 val empty = ""
 val copy = I

--- a/src/HOL/Import/import_package.ML	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/import_package.ML	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/import_package.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 signature IMPORT_PACKAGE =
 sig
     val import_meth: Args.src -> Proof.context -> Proof.method
@@ -5,6 +10,20 @@
     val debug      : bool ref
 end
 
+structure ImportDataArgs: THEORY_DATA_ARGS =
+struct
+val name = "HOL4/import_data"
+type T = ProofKernel.thm option array option
+val empty = None
+val copy = I
+val prep_ext = I
+fun merge _ = None
+fun print sg import_segment =
+    Pretty.writeln (Pretty.str ("Pretty printing of importer data not implemented"))
+end
+
+structure ImportData = TheoryDataFun(ImportDataArgs)
+
 structure ImportPackage :> IMPORT_PACKAGE =
 struct
 
@@ -24,7 +43,9 @@
 	    val sg = sign_of_thm th
 	    val prem = hd (prems_of th)
 	    val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem)))
-	    val int_thms = fst (Replay.setup_int_thms thyname thy)
+	    val int_thms = case ImportData.get thy of
+			       None => fst (Replay.setup_int_thms thyname thy)
+			     | Some a => a
 	    val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
 	    val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
 	    val thm = snd (ProofKernel.to_isa_thm hol4thm)
@@ -57,5 +78,5 @@
 			  Method.SIMPLE_METHOD (import_tac arg thy)
 		      end)
 
-val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem")]
+val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem"),ImportData.init]
 end

--- a/src/HOL/Import/import_syntax.ML	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/import_syntax.ML	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/import_syntax.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 signature HOL4_IMPORT_SYNTAX =
 sig
     type token = OuterSyntax.token
@@ -150,14 +155,26 @@
 	apply (set_replaying_thy s::Theory.add_path s::(fst (importP token_list)))
     end
 
+fun create_int_thms thyname thy =
+    case ImportData.get thy of
+	None => ImportData.put (Some (fst (Replay.setup_int_thms thyname thy))) thy
+      | Some _ => error "Import data not closed - forgotten an end_setup, mayhap?"
+
+fun clear_int_thms thy =
+    case ImportData.get thy of
+	None => error "Import data already cleared - forgotten a setup_theory?"
+      | Some _ => ImportData.put None thy
+
 val setup_theory = P.name
 		       >>
 		       (fn thyname =>
 			fn thy =>
-			   case HOL4DefThy.get thy of
-			       NoImport => thy |> import_thy thyname
-			     | Generating _ => error "Currently generating a theory!"
-			     | Replaying _ => thy |> clear_import_thy |> import_thy thyname)
+			   (case HOL4DefThy.get thy of
+				NoImport => thy
+			      | Generating _ => error "Currently generating a theory!"
+			      | Replaying _ => thy |> clear_import_thy)
+			       |> import_thy thyname
+			       |> create_int_thms thyname)
 
 fun end_setup toks =
     Scan.succeed
@@ -168,6 +185,7 @@
 	    in
 		thy |> set_segment thyname segname
 		    |> clear_import_thy
+		    |> clear_int_thms
 		    |> Theory.parent_path
 	    end) toks
 

--- a/src/HOL/Import/proof_kernel.ML	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/proof_kernel.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 signature ProofKernel =
 sig
     type hol_type
@@ -47,7 +52,7 @@
 
     exception PK of string * string
 
-    val get_proof_dir: string -> theory -> string
+    val get_proof_dir: string -> theory -> string option
     val debug : bool ref
     val disk_info_of : proof -> (string * string) option
     val set_disk_info_of : proof -> string -> string -> unit
@@ -165,16 +170,10 @@
 
 (* Compatibility. *)
 
-fun quote s = "\"" ^ s ^ "\""
-
-fun alphanum str = case String.explode str of
-		       first::rest => Char.isAlpha first andalso forall (fn c => Char.isAlphaNum c orelse c = #"_") rest
-		     | _ => error "ProofKernel.alphanum: Empty constname??"
-
-fun mk_syn c = if alphanum c then NoSyn else Syntax.literal c
+fun mk_syn c = if Symbol.is_identifier c then NoSyn else Syntax.literal c
 
 val keywords = ["open"]
-fun quotename c = if alphanum c andalso not (c mem keywords) then c else quote c
+fun quotename c = if Symbol.is_identifier c andalso not (c mem keywords) then c else quote c
 
 fun smart_string_of_cterm ct =
     let
@@ -321,6 +320,7 @@
 	    || scan_string "quot;" #"\""
 	    || scan_string "gt;" #">"
 	    || scan_string "lt;" #"<"
+            || scan_string "apos;" #"'"
 in
 fun scan_nonquote toks =
     case LazySeq.getItem toks of
@@ -566,29 +566,29 @@
 	    case get_segment2 thyname thy of
 		Some seg => seg
 	      | None => get_import_segment thy
-	val defpath = [(getenv "ISABELLE_HOME_USER") ^ "/proofs"]
-	val path =
-	    case getenv "PROOF_DIRS" of
-		"" => defpath
-	      | path => (space_explode ":" path) @ defpath
-	fun find [] = error ("Unable to find import segment " ^ import_segment)
-	  | find (p::ps) = (let
-				val dir = p ^ "/" ^ import_segment
-			    in
-				if OS.FileSys.isDir dir
-				then dir
-				else find ps
-			    end) handle OS.SysErr _ => find ps
+	val defpath = [OS.Path.joinDirFile {dir=getenv "ISABELLE_HOME_USER",file="proofs"}]
+	val path = space_explode ":" (getenv "PROOF_DIRS") @ defpath
+	fun find [] = None
+	  | find (p::ps) =
+	    (let
+		 val dir = OS.Path.joinDirFile {dir = p,file=import_segment}
+	     in
+		 if OS.FileSys.isDir dir
+		 then Some dir
+		 else find ps
+	     end) handle OS.SysErr _ => find ps
     in
-	find path ^ "/" ^ thyname
+	apsome (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path)
     end
 			   
 fun proof_file_name thyname thmname thy =
     let
-	val path = get_proof_dir thyname thy
+	val path = case get_proof_dir thyname thy of
+		       Some p => p
+		     | None => error "Cannot find proof files"
 	val _ = OS.FileSys.mkDir path handle OS.SysErr _ => ()
     in
-	String.concat[path,"/",thmname,".prf"]
+	OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = thmname, ext = SOME "prf"}}
     end
 	
 fun xml_to_proof thyname types terms prf thy =

--- a/src/HOL/Import/replay.ML	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/replay.ML	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/replay.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 structure Replay =
 struct
 
@@ -268,7 +273,11 @@
 
 fun setup_int_thms thyname thy =
     let
-	val is = TextIO.openIn(P.get_proof_dir thyname thy ^"/facts.lst")
+	val fname =
+	    case P.get_proof_dir thyname thy of
+		Some p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
+	      | None => error "Cannot find proof files"
+	val is = TextIO.openIn fname
 	val (num_int_thms,facts) =
 	    let
 		fun get_facts facts =

--- a/src/HOL/Import/shuffler.ML	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/shuffler.ML	Sat Apr 17 23:53:35 2004 +0200
@@ -1,7 +1,6 @@
-(*  Title:      Provers/shuffler.ML
+(*  Title:      HOL/Import/shuffler.ML
     ID:         $Id$
     Author:     Sebastian Skalberg, TU Muenchen
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Package for proving two terms equal by normalizing (hence the
 "shuffler" name).  Uses the simplifier for the normalization.

--- a/src/HOL/Tools/specification_package.ML	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Tools/specification_package.ML	Sat Apr 17 23:53:35 2004 +0200
@@ -1,7 +1,6 @@
 (*  Title:      HOL/Tools/specification_package.ML
     ID:         $Id$
     Author:     Sebastian Skalberg, TU Muenchen
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Package for defining constants by specification.
 *)