src/HOL/Import/replay.ML
changeset 33035 15eab423e573
parent 32970 fbd2bb2489a8
child 35742 eb8d2f668bfc
     1.1 --- a/src/HOL/Import/replay.ML	Tue Oct 20 23:25:04 2009 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Wed Oct 21 00:36:12 2009 +0200
     1.3 @@ -291,7 +291,7 @@
     1.4                  fun get_facts facts =
     1.5                      case TextIO.inputLine is of
     1.6                          NONE => (case facts of
     1.7 -                                   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
     1.8 +                                   i::facts => (the (Int.fromString i),map P.protect_factname (rev facts))
     1.9                                   | _ => raise ERR "replay_thm" "Bad facts.lst file")
    1.10                        | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
    1.11              in