diff -r 332a9f5c7c29 -r 13a9f54175ad src/HOL/Tools/ATP/watcher.ML
--- 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.