# HG changeset patch
# User smolkas
# Date 1367831132 -7200
# Node ID 46d911ab917041c51ca763f42b62f0ead2eb994c
# Parent  ee9562d317780987b1abd87bb659d6ccf42e4615
allow '-'s in tptp ids to avoid problems with remote_vampire

diff -r ee9562d31778 -r 46d911ab9170 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