1.1 --- a/src/HOL/Tools/TFL/tfl.ML Tue Oct 20 16:13:01 2009 +0200
1.2 +++ b/src/HOL/Tools/TFL/tfl.ML Wed Oct 21 08:14:38 2009 +0200
1.3 @@ -531,7 +531,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 (gen_union (op aconv)) [] TCl
1.8 + val TCs = List.foldr (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'