
diff -r 8b2c46e11674 -r 0fd4abb5fade Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Fri Dec 11 06:58:31 2009 +0100
+++ b/Quot/QuotMain.thy	Fri Dec 11 08:28:41 2009 +0100
@@ -5,7 +5,6 @@
      ("quotient_def.ML")
 begin
 
-
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -1021,10 +1020,10 @@
 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\n", qtrm_str, 
-             "and the lifted theorem\n", rtrm_str, "do not match"]
+  val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, 
+             "", "does not match with original theorem", rtrm_str]
 in
-  error (space_implode " " msg)
+  error msg
 end
 *}
 




