TFL/tfl.ML

       fun single [_$_] =
               mk_functional_err "recdef does not allow currying"
         | single [f] = f
         | single fs  =
               (*multiple function names?*)
-              if length (gen_distinct same_name fs) < length fs
+              if length (distinct same_name fs) < length fs
               then mk_functional_err
                    "The function being declared appears with multiple types"
               else mk_functional_err
                    (Int.toString (length fs) ^
                     " distinct function names being declared")

 fun mk_functional thy clauses =
  let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses
                    handle TERM _ => raise TFL_ERR "mk_functional"
                         "recursion equations must use the = relation")
      val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
-     val atom = single (gen_distinct (op aconv) funcs)
+     val atom = single (distinct (op aconv) funcs)
      val (fname,ftype) = dest_atom atom
      val dummy = map (no_repeat_vars thy) pats
      val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
                               map (fn (t,i) => (t,(i,true))) (enumerate R))
      val names = foldr add_term_names [] R