src/HOL/Tools/recfun_codegen.ML

 fun get_equations thy defs (s, T) =
   (case Symtab.lookup (RecCodegenData.get thy) s of
      NONE => ([], "")
    | SOME thms => 
        let val thms' = del_redundant thy []
-         (filter (fn (thm, _) => is_instance thy T
+         (filter (fn (thm, _) => is_instance T
            (snd (const_of (prop_of thm)))) thms)
        in if null thms' then ([], "")
          else (preprocess thy (map fst thms'),
            case snd (snd (split_last thms')) of
                NONE => (case get_defn thy defs s T of