# HG changeset patch
# User bulwahn
# Date 1319716351 -7200
# Node ID 252cd58847e031fdb717811cde24e319eb11fc8d
# Parent  728ed9d28c63bd7075af497521f286d3abf84797
respecting isabelle's programming style in the quotient package by simplifying qconsts_lookup function for data access; removing odd NotFound exception

diff -r 728ed9d28c63 -r 252cd58847e0 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 13:50:55 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 13:52:31 2011 +0200
@@ -8,7 +8,6 @@
 
 signature QUOTIENT_INFO =
 sig
-  exception NotFound  (* FIXME complicates signatures unnecessarily *)
 
   type maps_info = {mapfun: string, relmap: string}
   val maps_defined: theory -> string -> bool
@@ -27,8 +26,7 @@
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val transform_qconsts: morphism -> qconsts_info -> qconsts_info
-  (* FIXME functions called "lookup" must return option, not raise exception! *)
-  val qconsts_lookup: theory -> term -> qconsts_info     (* raises NotFound *)
+  val qconsts_lookup: theory -> term -> qconsts_info option
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory
   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
   val qconsts_dest: Proof.context -> qconsts_info list
@@ -49,9 +47,6 @@
 structure Quotient_Info: QUOTIENT_INFO =
 struct
 
-exception NotFound  (* FIXME odd OCaml-ism!? *)
-
-
 (** data containers **)
 
 (* FIXME just one data slot (record) per program unit *)
@@ -198,11 +193,8 @@
       end
   in
     (case Symtab.lookup (QConstsData.get thy) name of
-      NONE => raise NotFound
-    | SOME l =>
-        (case find_first matches l of
-          SOME x => x
-        | NONE => raise NotFound))
+      NONE => NONE
+    | SOME l => find_first matches l)
   end
 
 fun print_qconstinfo ctxt =
diff -r 728ed9d28c63 -r 252cd58847e0 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:50:55 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:52:31 2011 +0200
@@ -553,9 +553,9 @@
         if same_const rtrm qtrm then rtrm
         else
           let
-            val rtrm' = #rconst (Quotient_Info.qconsts_lookup thy qtrm)
-              handle Quotient_Info.NotFound =>
-                term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
+            val rtrm' = case Quotient_Info.qconsts_lookup thy qtrm of
+              SOME qconst_info => #rconst qconst_info
+            | NONE => 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