# HG changeset patch
# User blanchet
# Date 1337079975 -7200
# Node ID c35238d19bb967a9db11a3b57d23dbd7c0e412d0
# Parent  c6d5418ee7708aa68cad58a76f1aafa4bbe6effa
repair the Waldmeister endgame only for Waldmeister proofs

diff -r c6d5418ee770 -r c35238d19bb9 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 15 13:06:15 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue May 15 13:06:15 2012 +0200
@@ -318,7 +318,7 @@
   Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term))
                 dummy_inference
 
-val waldmeister_conjecture = "conjecture_1"
+val waldmeister_conjecture_name = "conjecture_1"
 
 val tofof_fact_prefix = "fof_"
 
@@ -380,7 +380,7 @@
               (* Waldmeister isn't exactly helping. *)
               case deps of
                 File_Source (_, SOME s) =>
-                (if s = waldmeister_conjecture then
+                (if s = waldmeister_conjecture_name then
                    case find_formula_in_problem problem (mk_anot phi) of
                      (* Waldmeister hack: Get the original orientation of the
                         equation to avoid confusing Isar. *)
diff -r c6d5418ee770 -r c35238d19bb9 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue May 15 13:06:15 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue May 15 13:06:15 2012 +0200
@@ -634,14 +634,16 @@
        pre @ map (replace_dependencies_in_line (name', [name])) post
      | _ => raise Fail "unexpected inference"
 
+val waldmeister_conjecture_num = "1.0.0.0"
+
 val repair_waldmeister_endgame =
   let
     fun do_tail (Inference_Step (name, t, rule, deps)) =
         Inference_Step (name, s_not t, rule, deps)
       | do_tail line = line
     fun do_body [] = []
-      | do_body ((line as Inference_Step ((_, ss), _, _, _)) :: lines) =
-        if is_conjecture ss then map do_tail (line :: lines)
+      | do_body ((line as Inference_Step ((num, _), _, _, _)) :: lines) =
+        if num = waldmeister_conjecture_num then map do_tail (line :: lines)
         else line :: do_body lines
       | do_body (line :: lines) = line :: do_body lines
   in do_body end