# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263554250 -3600
# Node ID 0f920b62fb7b27d28f64b298c20860f1700c9436
# Parent  cff21786d952097bcd0af65d8cb34e1f673d9dde
slight tuning of relation_error

diff -r cff21786d952 -r 0f920b62fb7b Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Fri Jan 15 11:04:21 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Jan 15 12:17:30 2010 +0100
@@ -377,6 +377,9 @@
     (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and>
     (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x)))
   )"
-apply (lifting hom)
+(*apply (lifting hom)*)
+sorry
+
+thm rlam.recs
 
 end
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 *)