diff -r 31509c8cf72e -r bdbb52979790 quotient_def.ML
--- a/quotient_def.ML	Sat Nov 21 03:12:50 2009 +0100
+++ b/quotient_def.ML	Sat Nov 21 10:58:08 2009 +0100
@@ -36,19 +36,30 @@
 
 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 
-fun ty_lift_error lthy rty qty =
+fun ty_strs lthy (ty1, ty2) = 
+  (quote (Syntax.string_of_typ lthy ty1),
+   quote (Syntax.string_of_typ lthy ty2))
+
+fun ty_lift_error1 lthy rty qty =
 let
-  val rty_str = quote (Syntax.string_of_typ lthy rty) 
-  val qty_str = quote (Syntax.string_of_typ lthy qty)
+  val (rty_str, qty_str) = ty_strs lthy (rty, qty) 
   val msg = ["quotient type", qty_str, "and lifted type", rty_str, "do not match."]
 in
   raise LIFT_MATCH (space_implode " " msg)
 end
 
+fun ty_lift_error2 lthy rty qty =
+let
+  val (rty_str, qty_str) = ty_strs lthy (rty, qty)   
+  val msg = ["No type variables allowed in", qty_str, "and", rty_str, "."]
+in
+  raise LIFT_MATCH (space_implode " " msg)
+end
+
 fun get_fun_aux lthy s fs =
   case (maps_lookup (ProofContext.theory_of lthy) s) of
     SOME info => list_comb (Const (#mapfun info, dummyT), fs)
-  | NONE      => raise LIFT_MATCH ("no map association for type " ^ s)
+  | NONE      => raise LIFT_MATCH (space_implode " " ["No map function for type", quote s, "."])
 
 fun get_const flag lthy _ qty =
 (* FIXME: check here that _ and qty are related *)
@@ -81,9 +92,9 @@
   | (TFree x, TFree x') =>
      if x = x'
      then mk_identity qty 
-     else ty_lift_error lthy rty qty
-  | (TVar _, TVar _) => raise LIFT_MATCH "no type variables allowed"
-  | _ => ty_lift_error lthy rty qty
+     else ty_lift_error1 lthy rty qty
+  | (TVar _, TVar _) => ty_lift_error2 lthy rty qty
+  | _ => ty_lift_error1 lthy rty qty
 
 fun make_def nconst_bname qty mx attr rhs lthy =
 let