# HG changeset patch
# User blanchet
# Date 1272536480 -7200
# Node ID 45c1870f234fba7857397b31b0ed8c291de8f5eb
# Parent  93b8ceabc923f3e5e298c816c17f80b03825091b
fixed definition of "bad frees" so that it actually works

diff -r 93b8ceabc923 -r 45c1870f234f src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 11:38:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 12:21:20 2010 +0200
@@ -525,18 +525,21 @@
 and delete_dep num lines =
   fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
 
-(* FIXME: this seems not to have worked and is obsolete anyway *)
-fun is_bad_free (Free (a, _)) = String.isPrefix skolem_prefix a
-  | is_bad_free _ = false
+(* ATPs sometimes reuse free variable names in the strangest ways. Surprisingly,
+   removing the offending lines often does the trick. *)
+fun is_bad_free frees (Free x) = not (member (op =) frees x)
+  | is_bad_free _ _ = false
 
-fun add_desired_line _ _ (line as Definition _) (j, lines) = (j, line :: lines)
-  | add_desired_line ctxt _ (Inference (num, t, [])) (j, lines) =
+fun add_desired_line _ _ _ (line as Definition _) (j, lines) =
+    (j, line :: lines)
+  | add_desired_line ctxt _ _ (Inference (num, t, [])) (j, lines) =
     (j, Inference (num, t, []) :: lines)  (* conjecture clauses must be kept *)
-  | add_desired_line ctxt shrink_factor (Inference (num, t, deps)) (j, lines) =
+  | add_desired_line ctxt shrink_factor frees (Inference (num, t, deps))
+                     (j, lines) =
     (j + 1,
      if is_only_type_information t orelse
         not (null (Term.add_tvars t [])) orelse
-        exists_subterm is_bad_free t orelse
+        exists_subterm (is_bad_free frees) t orelse
         (not (null lines) andalso (* last line must be kept *)
          (length deps < 2 orelse j mod shrink_factor <> 0)) then
        map (replace_deps_in_line (num, deps)) lines  (* delete line *)
@@ -640,7 +643,7 @@
       |> decode_lines ctxt
       |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
       |> rpair [] |-> fold_rev add_nontrivial_line
-      |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor)
+      |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor frees)
       |> snd
   in
     (if null frees then [] else [Fix frees]) @