changeset 926 | 9d1348498c36 |
parent 922 | 196ca0973a6d |
child 949 | 83c588d6fee9 |
--- a/src/Pure/sign.ML Fri Mar 03 12:04:45 1995 +0100 +++ b/src/Pure/sign.ML Fri Mar 03 12:34:57 1995 +0100 @@ -264,7 +264,7 @@ "\nInvolving these terms:\n" ^ cat_lines (map show_term ts); fun exn_type_msg (msg, Ts, ts) = - msg ^ "\nType checking error: " ^ msg ^ "\n" ^ + "\nType checking error: " ^ msg ^ "\n" ^ cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"; val T' = certify_typ sg T