diff -r 46d911ab9170 -r 475c2eab2d7c src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 06 11:05:32 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 06 11:17:33 2013 +0200
@@ -215,7 +215,7 @@
 (* Strings enclosed in single quotes (e.g., file names) *)
 val scan_general_id =
   $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
-  || Scan.repeat ($$ "$") -- Scan.many1 (fn s => Symbol.is_letdig s orelse s="-")
+  || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
      >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
 
 val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) >> implode