src/Pure/sign.ML
changeset 679 a682bbf70dc6
parent 623 ca9f5dbab880
child 763 d5a626aacdd3
     1.1 --- a/src/Pure/sign.ML	Wed Nov 02 09:09:30 1994 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Nov 02 10:45:14 1994 +0100
     1.3 @@ -255,8 +255,12 @@
     1.4        | term_err ts = 
     1.5            "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
     1.6  
     1.7 +    fun exn_type_msg (msg, Ts, ts) =
     1.8 +	msg ^ "\nType checking error: " ^ msg ^ "\n" ^
     1.9 +	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n";
    1.10 +
    1.11      val T' = certify_typ sg T
    1.12 -      handle TYPE (msg, _, _) => error msg;
    1.13 +      handle TYPE arg => error (exn_type_msg arg);
    1.14  
    1.15      val ct = const_type sg;
    1.16  
    1.17 @@ -265,9 +269,7 @@
    1.18  
    1.19               val ((infrd_t', tye'), msg') = 
    1.20                (mk_some (Type.infer_types (tsig, ct, types, sorts, T', t)), msg)
    1.21 -              handle TYPE (tmsg, Ts, ts) => 
    1.22 -                ((None, None), msg ^ "Type checking error: " ^ tmsg ^ "\n" ^
    1.23 -                 cat_lines (map show_typ Ts) ^ term_err ts ^ "\n")
    1.24 +              handle TYPE arg => ((None, None), exn_type_msg arg)
    1.25  
    1.26               val old_show_brackets = !show_brackets;
    1.27