# HG changeset patch
# User clasohm
# Date 794230497 -3600
# Node ID 9d1348498c366d537d858ce451debc45b88731ee
# Parent  15539deb68638ef34966e8ee7a8fd92a1a3c81d8
fixed a bug in infer_types/exn_type_msg

diff -r 15539deb6863 -r 9d1348498c36 src/Pure/sign.ML
--- 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