# HG changeset patch
# User haftmann
# Date 1163805633 -3600
# Node ID 3436c269dd2336c465b382c4afeee855ab1f5225
# Parent  8b15e5e668133f2a0599b32d922461acec870ae9
code thms for classops violating type discipline ignored

diff -r 8b15e5e66813 -r 3436c269dd23 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