# HG changeset patch
# User blanchet
# Date 1275491984 -7200
# Node ID 2f2f0d246d0f99281c1a48422e23d4da88844764
# Parent  0347b1a1668216e6ec3abd1b942e7967e5d7a1fb
handle Vampire's definitions smoothly

diff -r 0347b1a16682 -r 2f2f0d246d0f src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jun 02 17:06:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jun 02 17:19:44 2010 +0200
@@ -487,8 +487,8 @@
 fun decode_lines ctxt full_types tfrees lines =
   fst (fold_map (decode_line full_types tfrees) lines ctxt)
 
-fun aint_inference _ (Definition _) = true
-  | aint_inference t (Inference (_, t', _)) = not (t aconv t')
+fun aint_actual_inference _ (Definition _) = true
+  | aint_actual_inference t (Inference (_, t', _)) = not (t aconv t')
 
 (* No "real" literals means only type information (tfree_tcs, clsrel, or
    clsarity). *)
@@ -510,7 +510,7 @@
       if is_only_type_information t then
         map (replace_deps_in_line (num, [])) lines
       (* Is there a repetition? If so, replace later line by earlier one. *)
-      else case take_prefix (aint_inference t) lines of
+      else case take_prefix (aint_actual_inference t) lines of
         (_, []) => lines (*no repetition of proof line*)
       | (pre, Inference (num', _, _) :: post) =>
         pre @ map (replace_deps_in_line (num', [num])) post
@@ -523,7 +523,7 @@
     if is_only_type_information t then
       Inference (num, t, deps) :: lines
     (* Is there a repetition? If so, replace later line by earlier one. *)
-    else case take_prefix (aint_inference t) lines of
+    else case take_prefix (aint_actual_inference t) lines of
       (* FIXME: Doesn't this code risk conflating proofs involving different
          types?? *)
        (_, []) => Inference (num, t, deps) :: lines
@@ -539,8 +539,8 @@
 and delete_dep num lines =
   fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
 
-(* ATPs sometimes reuse free variable names in the strangest ways. Surprisingly,
-   removing the offending lines often does the trick. *)
+(* ATPs sometimes reuse free variable names in the strangest ways. Removing
+   offending lines often does the trick. *)
 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   | is_bad_free _ _ = false
 
@@ -549,8 +549,8 @@
                                         $ t1 $ t2)) = (t1 aconv t2)
   | is_trivial_formula t = false
 
-fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
-    (j, line :: lines)
+fun add_desired_line _ _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
+    (j, line :: map (replace_deps_in_line (num, [])) lines)
   | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
                      (Inference (num, t, deps)) (j, lines) =
     (j + 1,