improved warning
authorhaftmann
Fri Jan 04 09:04:32 2008 +0100 (2008-01-04)
changeset 258294b44d945702f
parent 25828 228c53fdb3b4
child 25830 8fbc7d38d6cf
improved warning
src/Pure/Isar/class.ML
src/Pure/Isar/instance.ML
     1.1 --- a/src/Pure/Isar/class.ML	Fri Jan 04 00:54:12 2008 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Jan 04 09:04:32 2008 +0100
     1.3 @@ -824,7 +824,7 @@
     1.4      val _ = case map (fst o snd) params
     1.5       of [] => ()
     1.6        | cs => Output.legacy_feature
     1.7 -          ("Missing definitions for overloaded parameters " ^ commas_quote cs)
     1.8 +          ("Missing specifications for overloaded parameters " ^ commas_quote cs)
     1.9    in lthy end;
    1.10  
    1.11  fun pretty_instantiation lthy =
     2.1 --- a/src/Pure/Isar/instance.ML	Fri Jan 04 00:54:12 2008 +0100
     2.2 +++ b/src/Pure/Isar/instance.ML	Fri Jan 04 09:04:32 2008 +0100
     2.3 @@ -47,7 +47,7 @@
     2.4          val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
     2.5        in Specification.definition def' ctxt end;
     2.6      val _ = if not (null defs) then Output.legacy_feature
     2.7 -      "Instance command with attached attached definitions; use instantiation instead." else ();
     2.8 +      "Instance command with attached definitions; use instantiation instead." else ();
     2.9    in if not (null defs) orelse forall (Class.is_class thy) sort
    2.10    then
    2.11      thy