Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/TFL/tfl.ML
changeset 33043 ff71cadefb14
parent 33040 cffdb7b28498
parent 33042 ddf1f03a9ad9
child 33063 4d462963a7db 
--- a/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 12:08:52 2009 +0200
@@ -531,7 +531,7 @@
                  then writeln (cat_lines ("Extractants =" ::
                   map (Display.string_of_thm_global thy) extractants))
                  else ()
-     val TCs = List.foldr (union (op aconv)) [] TCl
+     val TCs = List.foldr (uncurry (union (op aconv))) [] TCl
      val full_rqt = WFR::TCs
      val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
      val R'abs = S.rand R'
isabelle