# 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