--- a/src/HOL/Tools/ATP/atp_proof.ML Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon May 06 11:05:32 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 Symbol.is_letdig
+ || Scan.repeat ($$ "$") -- Scan.many1 (fn s => Symbol.is_letdig s orelse s="-")
>> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) >> implode