src/HOL/Tools/TFL/tfl.ML

--- a/src/HOL/Tools/TFL/tfl.ML	Thu Oct 29 23:49:55 2009 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Thu Oct 29 23:56:33 2009 +0100
@@ -529,7 +529,7 @@
                  then writeln (cat_lines ("Extractants =" ::
                   map (Display.string_of_thm_global thy) extractants))
                  else ()
-     val TCs = List.foldr (uncurry (union (op aconv))) [] TCl
+     val TCs = fold_rev (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'