--- 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 =
--- 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