diff -r cff21786d952 -r 0f920b62fb7b Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Jan 15 11:04:21 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Jan 15 12:17:30 2010 +0100
@@ -380,13 +380,13 @@
 
 fun relation_error ctxt r1 r2 =
 let
-  val r1s = Syntax.string_of_term ctxt r1
-  val r2s = Syntax.string_of_term ctxt r2
-  val r1t = Syntax.string_of_typ ctxt (fastype_of r1)
-  val r2t = Syntax.string_of_typ ctxt (fastype_of r2)
+  val r1_str = Syntax.string_of_term ctxt r1
+  val r2_str = Syntax.string_of_term ctxt r2
+  val r1_ty_str = Syntax.string_of_typ ctxt (fastype_of r1)
+  val r2_ty_str = Syntax.string_of_typ ctxt (fastype_of r2)
 in
-  raise LIFT_MATCH ("regularise (relation mismatch)\n[" ^
-  r1s ^ " :: " ^ r1t ^ "]\n[" ^ r2s ^ " :: " ^ r2t ^ "]")
+  raise LIFT_MATCH 
+    (cat_lines ["regularise (relation mismatch)", r1_str ^ "::" ^ r1_ty_str, r2_str ^ "::" ^ r2_ty_str])
 end
 
 (* the major type of All and Ex quantifiers *)