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