src/HOL/Import/replay.ML
changeset 14620 1be590fd2422
parent 14516 a183dec876ab
child 15531 08c8dad8e399
--- 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 =