1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 17:04:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 17:05:29 2011 +0200
     1.3 @@ -266,9 +266,18 @@
     1.4  
     1.5  (**** PARSING OF TSTP FORMAT ****)
     1.6  
     1.7 +(* FIXME: temporary hack *)
     1.8 +fun repair_waldmeister_step_name s =
     1.9 +  case space_explode "." s of
    1.10 +    [a, b, c, d] =>
    1.11 +    (case a of "0" => "X" | "1" => "Y" | _ => "Z" ^ a) ^
    1.12 +    (if size b = 1 then "0" else "") ^ b ^ c ^ d
    1.13 +  | _ => s
    1.14 +
    1.15  (* Strings enclosed in single quotes (e.g., file names) *)
    1.16  val scan_general_id =
    1.17 -  $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
    1.18 +  $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'"
    1.19 +     >> implode >> repair_waldmeister_step_name
    1.20    || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
    1.21       >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
    1.22