Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid renumbering hypotheses
authorblanchet
Mon, 06 Jun 2011 20:36:35 +0200
changeset 43192 9c29a00f2970
parent 43191 0a72c0527111
child 43193 e11bd628f1a5
avoid renumbering hypotheses
src/HOL/Tools/ATP/atp_translate.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle