# HG changeset patch
# User blanchet
# Date 1337003666 -7200
# Node ID b287682bf91714327c3f886eeae02b5cd981ed82
# Parent  d21c91239737d390d06743814bd5c2e53b57b4af
improve parsing of Waldmeister dependencies (and kill obsolete hack)

diff -r d21c91239737 -r b287682bf917 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 14 15:54:26 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 14 15:54:26 2012 +0200
@@ -217,18 +217,9 @@
 
 (**** PARSING OF TSTP FORMAT ****)
 
-(* FIXME: temporary hack *)
-fun repair_waldmeister_step_name s =
-  case space_explode "." s of
-    [a, b, c, d] =>
-    (case a of "0" => "X" | "1" => "Y" | _ => "Z" ^ a) ^
-    (if size b = 1 then "0" else "") ^ b ^ c ^ d
-  | _ => s
-
 (* Strings enclosed in single quotes (e.g., file names) *)
 val scan_general_id =
-  $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'"
-     >> implode >> repair_waldmeister_step_name
+  $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
   || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
      >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
 
@@ -252,7 +243,11 @@
 val dummy_phi = AAtom (ATerm ("", []))
 val dummy_inference = Inference_Source ("", [])
 
-fun parse_dependencies x = (skip_term ::: Scan.repeat ($$ "," |-- skip_term)) x
+(* "skip_term" is there to cope with Waldmeister nonsense such as
+   "theory(equality)". *)
+val parse_dependency = scan_general_id --| skip_term
+val parse_dependencies =
+  parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency)
 
 fun parse_source x =
   (Scan.this_string "file" |-- $$ "(" |-- scan_general_id --