--- a/QuotMain.thy	Wed Nov 25 15:20:10 2009 +0100
+++ b/QuotMain.thy	Wed Nov 25 15:43:12 2009 +0100
@@ -1118,8 +1118,8 @@
 let
   val rtrm_str = Syntax.string_of_term ctxt rtrm
   val qtrm_str = Syntax.string_of_term ctxt qtrm
-  val msg = [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, 
-             "and the lifted theorem", rtrm_str, "do not match"]
+  val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, 
+             "and the lifted theorem\n", rtrm_str, "do not match"]
 in
   error (space_implode " " msg)
 end