--- a/IntEx.thy	Sat Nov 21 03:12:50 2009 +0100
+++ b/IntEx.thy	Sat Nov 21 10:58:08 2009 +0100
@@ -8,7 +8,6 @@
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
 quotient my_int = "nat \<times> nat" / intrel
-  and    my_int' = "nat \<times> nat" / intrel
   apply(unfold EQUIV_def)
   apply(auto simp add: mem_def expand_fun_eq)
   done

--- 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

--- a/quotient_info.ML	Sat Nov 21 03:12:50 2009 +0100
+++ b/quotient_info.ML	Sat Nov 21 10:58:08 2009 +0100
@@ -45,6 +45,7 @@
 
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
+(* FIXME: this should be done using a generic context *)
 
 fun maps_attribute_aux s minfo = Thm.declaration_attribute 
   (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
@@ -95,13 +96,13 @@
 let
   fun prt_quot {qtyp, rtyp, rel, equiv_thm} = 
       Pretty.block (Library.separate (Pretty.brk 2)
-          [Pretty.str ("quotient type:"), 
+          [Pretty.str "quotient type:", 
            Syntax.pretty_typ ctxt qtyp,
-           Pretty.str ("raw type:"), 
+           Pretty.str "raw type:", 
            Syntax.pretty_typ ctxt rtyp,
-           Pretty.str ("relation:"), 
+           Pretty.str "relation:", 
            Syntax.pretty_term ctxt rel,
-           Pretty.str ("equiv. thm:"), 
+           Pretty.str "equiv. thm:", 
            Syntax.pretty_term ctxt (prop_of equiv_thm)])
 in
   QuotData.get (ProofContext.theory_of ctxt)
@@ -148,8 +149,7 @@
 val qconsts_lookup = Symtab.lookup o QConstsData.get
 
 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
-fun qconsts_update_gen k qcinfo = 
-      Context.mapping (qconsts_update_thy k qcinfo) I
+fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I
 
 fun print_qconstinfo ctxt =
 let
@@ -170,7 +170,6 @@
   OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
 
-
 end; (* structure *)
 
 open Quotient_Info