allow '-'s in tptp ids to avoid problems with remote_vampire
authorsmolkas
Mon, 06 May 2013 11:05:32 +0200
changeset 51880 46d911ab9170
parent 51879 ee9562d31778
child 51881 475c2eab2d7c
allow '-'s in tptp ids to avoid problems with remote_vampire
src/HOL/Tools/ATP/atp_proof.ML
--- 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