code thms for classops violating type discipline ignored
authorhaftmann
Sat, 18 Nov 2006 00:20:33 +0100
changeset 21421 3436c269dd23
parent 21420 8b15e5e66813
child 21422 25ed0a4c7dc5
code thms for classops violating type discipline ignored
src/Pure/Tools/codegen_data.ML
--- 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