src/HOL/Tools/TFL/tfl.ML
changeset 33339 d41f77196338
parent 33317 b4534348b8fd
child 33955 fff6f11b1f09
     1.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu Oct 29 23:49:55 2009 +0100
     1.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu Oct 29 23:56:33 2009 +0100
     1.3 @@ -529,7 +529,7 @@
     1.4                   then writeln (cat_lines ("Extractants =" ::
     1.5                    map (Display.string_of_thm_global thy) extractants))
     1.6                   else ()
     1.7 -     val TCs = List.foldr (uncurry (union (op aconv))) [] TCl
     1.8 +     val TCs = fold_rev (union (op aconv)) TCl []
     1.9       val full_rqt = WFR::TCs
    1.10       val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
    1.11       val R'abs = S.rand R'