changeset 24907 | bfb2e82b61fe |
parent 24624 | b8383b1bbae3 |
child 25389 | 3e58c7cb5a73 |
--- a/src/HOL/Tools/recfun_codegen.ML Mon Oct 08 18:13:05 2007 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Mon Oct 08 18:13:06 2007 +0200 @@ -67,7 +67,7 @@ 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'),