# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 9c29a00f297038738b1f29c85856c4ca24a74b77
# Parent  0a72c0527111972b9372e120a9c7610a3f7bc053
avoid renumbering hypotheses

diff -r 0a72c0527111 -r 9c29a00f2970 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -1399,7 +1399,9 @@
       |> ListPair.unzip
     (* Remove existing facts from the conjecture, as this can dramatically
        boost an ATP's performance (for some reason). *)
-    val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
+    val hyp_ts =
+      hyp_ts
+      |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
     val goal_t = Logic.list_implies (hyp_ts, concl_t)
     val all_ts = goal_t :: fact_ts
     val subs = tfree_classes_of_terms all_ts