src/HOL/Tools/TFL/tfl.ML

      val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
           handle Match => mk_functional_err "error in pattern-match translation"
      val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
      val finals = map row_of_pat patts2
      val originals = map (row_of_pat o #2) rows
-     val dummy = case (originals\\finals)
+     val dummy = case (subtract (op =) finals originals)
              of [] => ()
           | L => mk_functional_err
  ("The following clauses are redundant (covered by preceding clauses): " ^
                    commas (map (fn i => Int.toString (i + 1)) L))
  in {functional = Abs(Long_Name.base_name fname, ftype,