src/HOL/Import/replay.ML
changeset 23139 aa899bce7c3b
parent 21078 101aefd61aac
child 24712 64ed05609568
     1.1 --- a/src/HOL/Import/replay.ML	Wed May 30 23:32:54 2007 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Thu May 31 01:25:24 2007 +0200
     1.3 @@ -291,10 +291,10 @@
     1.4  	    let
     1.5  		fun get_facts facts =
     1.6  		    case TextIO.inputLine is of
     1.7 -			"" => (case facts of
     1.8 +			NONE => (case facts of
     1.9  				   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
    1.10  				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
    1.11 -		      | fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
    1.12 +		      | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
    1.13  	    in
    1.14  		get_facts []
    1.15  	    end