changeset 21421 | 3436c269dd23 |
parent 21338 | 56d55dd30311 |
child 21708 | 45e7491bea47 |
--- a/src/Pure/Tools/codegen_data.ML Sat Nov 18 00:20:29 2006 +0100 +++ b/src/Pure/Tools/codegen_data.ML Sat Nov 18 00:20:33 2006 +0100 @@ -175,7 +175,9 @@ in if Sign.typ_equiv thy (ty_decl, ty) then SOME (const, thm) else (if is_classop - then error + then if !strict_functyp + then error + else warning #> K NONE else if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) then warning #> (K o SOME) (const, thm) else if !strict_functyp