# HG changeset patch # User haftmann # Date 1180552157 -7200 # Node ID 9f01af828a10a70ca865348c2fd04bc5ddbf9ee8 # Parent 6cd88d27f600097e959d9a98c4b5d4f1f47f8fc6 instance: always print sorts on failure diff -r 6cd88d27f600 -r 9f01af828a10 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Wed May 30 21:09:16 2007 +0200 +++ b/src/Pure/Tools/class_package.ML Wed May 30 21:09:17 2007 +0200 @@ -179,7 +179,8 @@ | SOME name => name; val t' = case mk_typnorm thy_read (ty', ty) of NONE => error ("illegal definition for constant " ^ - quote c ^ "::" ^ Sign.string_of_typ thy_read ty) + quote (c ^ "::" ^ setmp show_sorts true + (Sign.string_of_typ thy_read) ty)) | SOME norm => map_types norm t in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end; in fold_map read defs cs end;