# HG changeset patch
# User wenzelm
# Date 1191244494 -7200
# Node ID fd4655e57168d06c1e49a221c393167ab31378ac
# Parent  fb1830099265ef14619ec4d9be447e518a057ff8
tuned message;

diff -r fb1830099265 -r fd4655e57168 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Mon Oct 01 15:14:53 2007 +0200
+++ b/src/Pure/defs.ML	Mon Oct 01 15:14:54 2007 +0200
@@ -98,7 +98,7 @@
 fun disjoint_specs c (i, {lhs = Ts, name = a, ...}: spec) =
   Inttab.forall (fn (j, {lhs = Us, name = b, ...}: spec) =>
     i = j orelse disjoint_args (Ts, Us) orelse
-      error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
+      error ("Clash of specifications " ^ quote a ^ " and " ^ quote b ^
         " for constant " ^ quote c));
 
 fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =