src/Pure/sign.ML
changeset 3552 f348e8a2db4b
parent 2979 db6941221197
child 3791 c5db2c87a646
     1.1 --- a/src/Pure/sign.ML	Tue Jul 22 18:46:44 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Jul 22 19:33:30 1997 +0200
     1.3 @@ -241,7 +241,7 @@
     1.4  (*read and certify typ wrt a signature*)
     1.5  fun read_typ (Sg {tsig, syn, ...}, sort_of) str =
     1.6    Type.cert_typ tsig (read_raw_typ syn tsig sort_of str)
     1.7 -    handle TYPE (msg, _, _) => (writeln msg; err_in_type str);
     1.8 +    handle TYPE (msg, _, _) => (error_msg msg; err_in_type str);
     1.9  
    1.10  
    1.11  
    1.12 @@ -371,7 +371,7 @@
    1.13      (case foldl process_term (Errs [], ts ~~ (0 upto (length ts - 1))) of
    1.14        One res =>
    1.15         (if length ts > ! Syntax.ambiguity_level then
    1.16 -          writeln "Fortunately, only one parse tree is type correct.\n\
    1.17 +          warning "Fortunately, only one parse tree is type correct.\n\
    1.18              \It helps (speed!) if you disambiguate your grammar or your input."
    1.19          else (); res)
    1.20      | Errs errs => (warn (); error (cat_lines errs))
    1.21 @@ -454,7 +454,7 @@
    1.22      fun prep_const (c, ty, mx) =
    1.23       (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
    1.24         handle TYPE (msg, _, _)
    1.25 -         => (writeln msg; err_in_const (Syntax.const_name c mx));
    1.26 +         => (error_msg msg; err_in_const (Syntax.const_name c mx));
    1.27  
    1.28      val consts = map (prep_const o rd_const syn tsig) raw_consts;
    1.29      val decls =