src/Pure/Tools/codegen_data.ML

           (snd o CodegenConsts.typ_of_inst thy) const;
         val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
       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
             then error
           else warning #> K NONE)