--- a/src/HOL/Tools/ATP/watcher.ML Tue Jun 26 18:28:40 2007 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Tue Jun 26 18:32:24 2007 +0200
@@ -191,10 +191,10 @@
(*get the number of the subgoal from the filename: the last digit string*)
fun number_from_filename s =
- case String.tokens (not o Char.isDigit) s of
- [] => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
- error "")
- | numbers => valOf (Int.fromString (List.last numbers));
+ let val numbers = "xxx" :: String.tokens (not o Char.isDigit) s
+ in valOf (Int.fromString (List.last numbers)) end
+ handle Option => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
+ error ("Watcher could not read subgoal nunber! " ^ s));
(*Call ATP. Settings should be a list of strings ["-t 300", "-m 100000"],
which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.