# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259160192 -3600
# Node ID aa452130ae7f004afc09242ece4c46870197db8b
# Parent  f78aa16daae576fd56af2fbfb6fca6b67a9c43e6
polishing

diff -r f78aa16daae5 -r aa452130ae7f QuotMain.thy
--- 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