diff -r fe3f227a59cd -r 2fb07e01c57b Quot/quotient_term.ML
--- 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 =