# HG changeset patch
# User haftmann
# Date 1199433872 -3600
# Node ID 4b44d945702f7076bc2dc55870c0da5baa8050f1
# Parent  228c53fdb3b426dde5599388b1d01fc9d3f78e1f
improved warning

diff -r 228c53fdb3b4 -r 4b44d945702f src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Jan 04 00:54:12 2008 +0100
+++ b/src/Pure/Isar/class.ML	Fri Jan 04 09:04:32 2008 +0100
@@ -824,7 +824,7 @@
     val _ = case map (fst o snd) params
      of [] => ()
       | cs => Output.legacy_feature
-          ("Missing definitions for overloaded parameters " ^ commas_quote cs)
+          ("Missing specifications for overloaded parameters " ^ commas_quote cs)
   in lthy end;
 
 fun pretty_instantiation lthy =
diff -r 228c53fdb3b4 -r 4b44d945702f src/Pure/Isar/instance.ML
--- a/src/Pure/Isar/instance.ML	Fri Jan 04 00:54:12 2008 +0100
+++ b/src/Pure/Isar/instance.ML	Fri Jan 04 09:04:32 2008 +0100
@@ -47,7 +47,7 @@
         val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
       in Specification.definition def' ctxt end;
     val _ = if not (null defs) then Output.legacy_feature
-      "Instance command with attached attached definitions; use instantiation instead." else ();
+      "Instance command with attached definitions; use instantiation instead." else ();
   in if not (null defs) orelse forall (Class.is_class thy) sort
   then
     thy