src/HOL/Tools/TFL/tfl.ML

--- a/src/HOL/Tools/TFL/tfl.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -342,8 +342,7 @@
  ("The following clauses are redundant (covered by preceding clauses): " ^
                    commas (map (fn i => string_of_int (i + 1)) L))
  in {functional = Abs(Long_Name.base_name fname, ftype,
-                      abstract_over (atom,
-                                     absfree(aname,atype, case_tm))),
+                      abstract_over (atom, absfree (aname,atype) case_tm)),
      pats = patts2}
 end end;