# HG changeset patch
# User blanchet
# Date 1306249529 -7200
# Node ID 6b39a2098ffd1deed0f7c4fd884501f06558b534
# Parent  79c191d3ea031aebfcc968fbdb20f8e32b1e48c7
hack to obtain potable step names from Waldmeister

diff -r 79c191d3ea03 -r 6b39a2098ffd src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 17:04:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 17:05:29 2011 +0200
@@ -266,9 +266,18 @@
 
 (**** 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
+  $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'"
+     >> implode >> repair_waldmeister_step_name
   || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
      >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)