diff -r f64d826a3f55 -r fe3f227a59cd Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Tue Feb 09 15:28:30 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Feb 09 15:36:23 2010 +0100
@@ -65,7 +65,7 @@
 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 NotFound => raise exc
+  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exc
 in
   Const (mapfun, dummyT)
 end
@@ -102,7 +102,7 @@
 let
   val thy = ProofContext.theory_of ctxt
   val exc = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
-  val qdata = (quotdata_lookup thy s) handle NotFound => raise exc
+  val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exc
 in
   (#rtyp qdata, #qtyp qdata)
 end
@@ -270,7 +270,7 @@
 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 NotFound => raise exc
+  val relmap =  #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exc
 in
   Const (relmap, dummyT)
 end
@@ -294,7 +294,7 @@
   val thy = ProofContext.theory_of ctxt
   val exc = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") 
 in
-  #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exc
+  #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exc
 end
 
 fun equiv_match_err ctxt ty_pat ty =
@@ -552,7 +552,7 @@
          else
            let
              val rtrm' = #rconst (qconsts_lookup thy qtrm)
-               handle NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
+               handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
            in
              if Pattern.matches thy (rtrm', rtrm)
              then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm