src/Pure/sign.ML
changeset 926 9d1348498c36
parent 922 196ca0973a6d
child 949 83c588d6fee9
equal deleted inserted replaced
925:15539deb6863 926:9d1348498c36
   262       | term_err [t] = "\nInvolving this term:\n" ^ show_term t
   262       | term_err [t] = "\nInvolving this term:\n" ^ show_term t
   263       | term_err ts = 
   263       | term_err ts = 
   264           "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
   264           "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
   265 
   265 
   266     fun exn_type_msg (msg, Ts, ts) =
   266     fun exn_type_msg (msg, Ts, ts) =
   267 	msg ^ "\nType checking error: " ^ msg ^ "\n" ^
   267 	"\nType checking error: " ^ msg ^ "\n" ^
   268 	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n";
   268 	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n";
   269 
   269 
   270     val T' = certify_typ sg T
   270     val T' = certify_typ sg T
   271       handle TYPE arg => error (exn_type_msg arg);
   271       handle TYPE arg => error (exn_type_msg arg);
   272 
   272