src/HOL/Import/replay.ML
changeset 23139 aa899bce7c3b
parent 21078 101aefd61aac
child 24712 64ed05609568
equal deleted inserted replaced
23138:6852373aae8a 23139:aa899bce7c3b
   289 	val is = TextIO.openIn fname
   289 	val is = TextIO.openIn fname
   290 	val (num_int_thms,facts) =
   290 	val (num_int_thms,facts) =
   291 	    let
   291 	    let
   292 		fun get_facts facts =
   292 		fun get_facts facts =
   293 		    case TextIO.inputLine is of
   293 		    case TextIO.inputLine is of
   294 			"" => (case facts of
   294 			NONE => (case facts of
   295 				   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
   295 				   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
   296 				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
   296 				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
   297 		      | fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
   297 		      | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
   298 	    in
   298 	    in
   299 		get_facts []
   299 		get_facts []
   300 	    end
   300 	    end
   301 	val _ = TextIO.closeIn is
   301 	val _ = TextIO.closeIn is
   302 	val int_thms = Array.array(num_int_thms,NONE:thm option)
   302 	val int_thms = Array.array(num_int_thms,NONE:thm option)