diff -r ee83040c3c84 -r c96ec8dd06a9 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Wed Mar 08 16:29:07 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Mar 08 17:03:19 2006 +0100
@@ -805,7 +805,8 @@
                      instant_itype (instant (v, tyco `%% map (ITyVar o fst) arity)) ty),
                   (sortctxt', ty'))
                 then (m, (m', (check_funeqs eqs, (sortctxt', ty'))))
-                else error ("inconsistent type for member definition " ^ quote m)
+                else (m, (m', (check_funeqs eqs, (sortctxt', ty'))))
+(*                 error ("inconsistent type for member definition " ^ quote m)  *)
       in Classinst (d, map mk_memdef membrs) end
   | check_prep_def modl Classinstmember =
       error "attempted to add bare class instance member";