# HG changeset patch
# User haftmann
# Date 1170255917 -3600
# Node ID 69d4b98f4c474934c09eaa92e36d2a5ad7dbc988
# Parent  bb07dd6cb1b95654b9c6794aa5ba7876c895e072
clarified error message

diff -r bb07dd6cb1b9 -r 69d4b98f4c47 src/Pure/Tools/codegen_funcgr.ML
--- a/src/Pure/Tools/codegen_funcgr.ML	Wed Jan 31 16:05:16 2007 +0100
+++ b/src/Pure/Tools/codegen_funcgr.ML	Wed Jan 31 16:05:17 2007 +0100
@@ -260,7 +260,7 @@
       | NONE => (case AxClass.class_of_param thy c
          of SOME class => classop_typ const class
           | NONE => Sign.the_const_type thy c)
-    fun typ_func (const as (c, tys)) thm =
+    fun typ_func (const as (c, tys)) thms thm =
       let
         val ty = CodegenFunc.typ_func thm;
       in case AxClass.class_of_param thy c
@@ -270,13 +270,15 @@
               else raise raise INVALID ([const], "Illegal instantation for class operation "
                     ^ CodegenConsts.string_of_const thy const
                     ^ ":\n" ^ CodegenConsts.string_of_typ thy ty_decl
-                    ^ "\nto " ^ CodegenConsts.string_of_typ thy ty)
+                    ^ "\nto " ^ CodegenConsts.string_of_typ thy ty
+                    ^ "\nin defining equations\n"
+                    ^ (cat_lines o map string_of_thm) thms)
               end
             | _ => ty)
         | NONE => ty
       end;
     fun add_funcs (const, thms as thm :: _) =
-          Constgraph.new_node (const, (typ_func const thm, thms))
+          Constgraph.new_node (const, (typ_func const thms thm, thms))
       | add_funcs (const, []) =
           Constgraph.new_node (const, (default_typ const, []));
     fun add_deps (funcs as (const, thms)) funcgr =