# HG changeset patch
# User bulwahn
# Date 1319716254 -7200
# Node ID 5995ab88a00fa87a7bd349d8115fb449f8c45a0b
# Parent  8f204549c2a5d56640cedab7895f2cc108ceaaf4
respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access

diff -r 8f204549c2a5 -r 5995ab88a00f src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Oct 27 07:48:07 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Oct 27 13:50:54 2011 +0200
@@ -642,7 +642,7 @@
       |> Option.map snd |> these |> null |> not
   | is_codatatype _ _ = false
 fun is_real_quot_type thy (Type (s, _)) =
-    is_some (Quotient_Info.quotdata_lookup_raw thy s)
+    is_some (Quotient_Info.quotdata_lookup thy s)
   | is_real_quot_type _ _ = false
 fun is_quot_type ctxt T =
   let val thy = Proof_Context.theory_of ctxt in
@@ -738,15 +738,14 @@
      | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
   | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
 fun rep_type_for_quot_type thy (T as Type (s, _)) =
-    let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
+    let val {qtyp, rtyp, ...} = the (Quotient_Info.quotdata_lookup thy s) in
       instantiate_type thy qtyp T rtyp
     end
   | rep_type_for_quot_type _ T =
     raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
 fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
     let
-      val {qtyp, equiv_rel, equiv_thm, ...} =
-        Quotient_Info.quotdata_lookup thy s
+      val {qtyp, equiv_rel, equiv_thm, ...} = the (Quotient_Info.quotdata_lookup thy s)
       val partial =
         case prop_of equiv_thm of
           @{const Trueprop} $ (Const (@{const_name equivp}, _) $ _) => false
diff -r 8f204549c2a5 -r 5995ab88a00f src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 07:48:07 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 13:50:54 2011 +0200
@@ -20,8 +20,7 @@
 
   type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
   val transform_quotdata: morphism -> quotdata_info -> quotdata_info
-  val quotdata_lookup_raw: theory -> string -> quotdata_info option
-  val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
+  val quotdata_lookup: theory -> string -> quotdata_info option
   val quotdata_update_thy: string -> quotdata_info -> theory -> theory
   val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
   val quotdata_dest: Proof.context -> quotdata_info list
@@ -136,12 +135,7 @@
    equiv_rel = Morphism.term phi equiv_rel,
    equiv_thm = Morphism.thm phi equiv_thm}
 
-fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str
-
-fun quotdata_lookup thy str =
-  case Symtab.lookup (QuotData.get thy) str of
-    SOME qinfo => qinfo
-  | NONE => raise NotFound
+fun quotdata_lookup thy str = Symtab.lookup (QuotData.get thy) str
 
 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
diff -r 8f204549c2a5 -r 5995ab88a00f src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 07:48:07 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:50:54 2011 +0200
@@ -100,13 +100,9 @@
    a quotient definition
 *)
 fun get_rty_qty ctxt s =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound =>
-      raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
-  in
-    (#rtyp qdata, #qtyp qdata)
-  end
+  case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
+    SOME qdata => (#rtyp qdata, #qtyp qdata)
+  | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.");
 
 (* takes two type-environments and looks
    up in both of them the variable v, which
@@ -302,12 +298,9 @@
   end
 
 fun get_equiv_rel ctxt s =
-  let
-    val thy = Proof_Context.theory_of ctxt
-  in
-    #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound =>
-      raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
-  end
+  case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
+      SOME qdata => #equiv_rel qdata
+    | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
 
 fun equiv_match_err ctxt ty_pat ty =
   let
@@ -442,7 +435,7 @@
           if length rtys <> length qtys then false
           else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
         else
-          (case Quotient_Info.quotdata_lookup_raw thy qs of
+          (case Quotient_Info.quotdata_lookup thy qs of
             SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
           | NONE => false)
     | _ => false)