# HG changeset patch
# User wenzelm
# Date 1288296666 -7200
# Node ID 8694a12611f9bfe6df8c594a37905c94612b9c8b
# Parent  87998864284eb6b326c60e9853e3d8bd66a9dbb7
handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable;
clarified handle/raise wrt. Quotient_Info.NotFound -- avoid fragile unqualified NotFound depending on "open" scope;
added helpful comments;

diff -r 87998864284e -r 8694a12611f9 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 28 22:04:00 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 28 22:11:06 2010 +0200
@@ -6,10 +6,11 @@
 
 signature QUOTIENT_INFO =
 sig
-  exception NotFound
+  exception NotFound  (* FIXME complicates signatures unnecessarily *)
 
   type maps_info = {mapfun: string, relmap: string}
   val maps_defined: theory -> string -> bool
+  (* FIXME functions called "lookup" must return option, not raise exception *)
   val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)
   val maps_update_thy: string -> maps_info -> theory -> theory
   val maps_update: string -> maps_info -> Proof.context -> Proof.context
diff -r 87998864284e -r 8694a12611f9 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 28 22:04:00 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 28 22:11:06 2010 +0200
@@ -67,8 +67,8 @@
 fun get_mapfun ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
-  val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exn
+  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound =>
+    raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
 in
   Const (mapfun, dummyT)
 end
@@ -104,8 +104,8 @@
 fun get_rty_qty ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
-  val qdata = quotdata_lookup thy s handle NotFound => raise exn
+  val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
+    raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
 in
   (#rtyp qdata, #qtyp qdata)
 end
@@ -127,7 +127,7 @@
   val thy = ProofContext.theory_of ctxt
 in
   Sign.typ_match thy (ty_pat, ty) Vartab.empty
-  handle MATCH_TYPE => err ctxt ty_pat ty
+  handle Type.TYPE_MATCH => err ctxt ty_pat ty
 end
 
 (* produces the rep or abs constant for a qty *)
@@ -276,8 +276,8 @@
 fun get_relmap ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
-  val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exn
+  val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
+    raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
 in
   Const (relmap, dummyT)
 end
@@ -299,9 +299,9 @@
 fun get_equiv_rel ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
-  val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
 in
-  #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exn
+  #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
+    raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
 end
 
 fun equiv_match_err ctxt ty_pat ty =
@@ -563,7 +563,8 @@
          else
            let
              val rtrm' = #rconst (qconsts_lookup thy qtrm)
-               handle NotFound => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
+               handle Quotient_Info.NotFound =>
+                term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
            in
              if Pattern.matches thy (rtrm', rtrm)
              then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm