src/HOL/Tools/ATP/atp_proof_reconstruct.ML

--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 14 15:54:26 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 14 15:54:26 2012 +0200
@@ -593,7 +593,7 @@
 
 (* No "real" literals means only type information (tfree_tcs, clsrel, or
    clsarity). *)
-val is_only_type_information = curry (op aconv) @{term True}
+fun is_only_type_information t = t aconv @{term True}
 
 fun replace_one_dependency (old, new) dep =
   if is_same_atp_step dep old then new else [dep]
@@ -619,7 +619,7 @@
         pre @ map (replace_dependencies_in_line (name', [name])) post
       | _ => raise Fail "unexpected inference"
     else if is_conjecture ss then
-      Inference_Step (name, s_not t, rule, []) :: lines
+      Inference_Step (name, t, rule, []) :: lines
     else
       map (replace_dependencies_in_line (name, [])) lines
   | add_line _ (Inference_Step (name, t, rule, deps)) lines =
@@ -636,6 +636,18 @@
        pre @ map (replace_dependencies_in_line (name', [name])) post
      | _ => raise Fail "unexpected inference"
 
+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)
+        else line :: do_body lines
+      | do_body (line :: lines) = line :: do_body lines
+  in do_body end
+
 (* Recursively delete empty lines (type information) from the proof. *)
 fun add_nontrivial_line (line as Inference_Step (name, t, _, [])) lines =
     if is_only_type_information t then delete_dependency name lines
@@ -864,6 +876,7 @@
           |> map_term_names_in_atp_proof repair_name
           |> decode_lines ctxt sym_tab
           |> rpair [] |-> fold_rev (add_line fact_names)
+          |> repair_waldmeister_endgame
           |> rpair [] |-> fold_rev add_nontrivial_line
           |> rpair (0, [])
           |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees)
@@ -884,9 +897,9 @@
           |> fold (fn Definition_Step _ => I (* FIXME *)
                     | Inference_Step ((s, _), t, _, _) =>
                       Symtab.update_new (s,
-                          t |> member (op = o apsnd fst) tainted s ? s_not))
+                          t |> fold_rev forall_of (map Var (Term.add_vars t []))
+                            |> member (op = o apsnd fst) tainted s ? s_not))
                   atp_proof
-        (* FIXME: add "fold_rev forall_of (map Var (Term.add_vars t []))"? *)
         fun prop_of_clause c =
           fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
                @{term False}