--- a/QuotMain.thy	Sat Nov 21 02:53:23 2009 +0100
+++ b/QuotMain.thy	Sat Nov 21 03:12:50 2009 +0100
@@ -1203,8 +1203,6 @@
 (* version with explicit qtrm             *)
 (******************************************)
 
-(* exception for when qtrm and rtrm do not match *)
-
 ML {*
 fun mk_resp_arg lthy (rty, qty) =
 let
@@ -1236,6 +1234,17 @@
 *}
 
 ML {*
+fun trm_lift_error lthy rtrm qtrm =
+let
+  val rtrm_str = quote (Syntax.string_of_term lthy rtrm) 
+  val qtrm_str = quote (Syntax.string_of_term lthy qtrm)
+  val msg = ["quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."]
+in
+  raise LIFT_MATCH (space_implode " " msg)
+end 
+*}
+
+ML {*
 (* applies f to the subterm of an abstractions, otherwise to the given term *)
 (* abstracted variables do not have to be treated specially *)
 fun apply_subt f trm1 trm2 =
@@ -1303,16 +1312,16 @@
   | (Free (x, ty), Free (x', ty')) =>
        if x = x' 
        then rtrm 
-       else raise LIFT_MATCH "quotient and lifted theorem do not match"
+       else trm_lift_error lthy rtrm qtrm
   | (Bound i, Bound i') =>
        if i = i' 
        then rtrm 
-       else raise LIFT_MATCH "quotient and lifted theorem do not match"
+       else trm_lift_error lthy rtrm qtrm
   | (Const (s, ty), Const (s', ty')) =>
        if s = s' andalso ty = ty'
        then rtrm
        else rtrm (* FIXME: check correspondence according to definitions *) 
-  | _ => raise LIFT_MATCH "quotient and lifted theorem do not match"
+  | _ => trm_lift_error lthy rtrm qtrm
 *}
 
 ML {*