author | haftmann |
Sat, 18 Nov 2006 00:20:33 +0100 | |
changeset 21421 | 3436c269dd23 |
parent 21420 | 8b15e5e66813 |
child 21422 | 25ed0a4c7dc5 |
--- 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