src/HOL/Import/replay.ML
changeset 14620 1be590fd2422
parent 14516 a183dec876ab
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Import/replay.ML	Sat Apr 17 20:04:23 2004 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Sat Apr 17 23:53:35 2004 +0200
     1.3 @@ -1,3 +1,8 @@
     1.4 +(*  Title:      HOL/Import/replay.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     1.7 +*)
     1.8 +
     1.9  structure Replay =
    1.10  struct
    1.11  
    1.12 @@ -268,7 +273,11 @@
    1.13  
    1.14  fun setup_int_thms thyname thy =
    1.15      let
    1.16 -	val is = TextIO.openIn(P.get_proof_dir thyname thy ^"/facts.lst")
    1.17 +	val fname =
    1.18 +	    case P.get_proof_dir thyname thy of
    1.19 +		Some p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
    1.20 +	      | None => error "Cannot find proof files"
    1.21 +	val is = TextIO.openIn fname
    1.22  	val (num_int_thms,facts) =
    1.23  	    let
    1.24  		fun get_facts facts =