--- a/Quot/quotient_info.ML	Tue Feb 09 15:36:23 2010 +0100
+++ b/Quot/quotient_info.ML	Tue Feb 09 15:43:39 2010 +0100
@@ -110,7 +110,7 @@
   val relname = Sign.intern_const thy relstr
 
   fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
-  val _ =  List.app sanity_check [mapname, relname]
+  val _ = List.app sanity_check [mapname, relname]
 in
   maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
 end

--- a/Quot/quotient_term.ML	Tue Feb 09 15:36:23 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Feb 09 15:43:39 2010 +0100
@@ -64,8 +64,8 @@
 fun get_mapfun ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exc = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
-  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exc
+  val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
+  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
 in
   Const (mapfun, dummyT)
 end
@@ -101,8 +101,8 @@
 fun get_rty_qty ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exc = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
-  val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exc
+  val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
+  val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
 in
   (#rtyp qdata, #qtyp qdata)
 end
@@ -269,8 +269,8 @@
 fun get_relmap ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exc =  LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") 
-  val relmap =  #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exc
+  val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") 
+  val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
 in
   Const (relmap, dummyT)
 end
@@ -292,9 +292,9 @@
 fun get_equiv_rel ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exc = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") 
+  val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") 
 in
-  #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exc
+  #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
 end
 
 fun equiv_match_err ctxt ty_pat ty =