1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Oct 27 07:48:07 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Oct 27 13:50:54 2011 +0200
     1.3 @@ -642,7 +642,7 @@
     1.4        |> Option.map snd |> these |> null |> not
     1.5    | is_codatatype _ _ = false
     1.6  fun is_real_quot_type thy (Type (s, _)) =
     1.7 -    is_some (Quotient_Info.quotdata_lookup_raw thy s)
     1.8 +    is_some (Quotient_Info.quotdata_lookup thy s)
     1.9    | is_real_quot_type _ _ = false
    1.10  fun is_quot_type ctxt T =
    1.11    let val thy = Proof_Context.theory_of ctxt in
    1.12 @@ -738,15 +738,14 @@
    1.13       | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
    1.14    | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
    1.15  fun rep_type_for_quot_type thy (T as Type (s, _)) =
    1.16 -    let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
    1.17 +    let val {qtyp, rtyp, ...} = the (Quotient_Info.quotdata_lookup thy s) in
    1.18        instantiate_type thy qtyp T rtyp
    1.19      end
    1.20    | rep_type_for_quot_type _ T =
    1.21      raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
    1.22  fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
    1.23      let
    1.24 -      val {qtyp, equiv_rel, equiv_thm, ...} =
    1.25 -        Quotient_Info.quotdata_lookup thy s
    1.26 +      val {qtyp, equiv_rel, equiv_thm, ...} = the (Quotient_Info.quotdata_lookup thy s)
    1.27        val partial =
    1.28          case prop_of equiv_thm of
    1.29            @{const Trueprop} $ (Const (@{const_name equivp}, _) $ _) => false

     2.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 07:48:07 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 13:50:54 2011 +0200
     2.3 @@ -20,8 +20,7 @@
     2.4  
     2.5    type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
     2.6    val transform_quotdata: morphism -> quotdata_info -> quotdata_info
     2.7 -  val quotdata_lookup_raw: theory -> string -> quotdata_info option
     2.8 -  val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
     2.9 +  val quotdata_lookup: theory -> string -> quotdata_info option
    2.10    val quotdata_update_thy: string -> quotdata_info -> theory -> theory
    2.11    val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
    2.12    val quotdata_dest: Proof.context -> quotdata_info list
    2.13 @@ -136,12 +135,7 @@
    2.14     equiv_rel = Morphism.term phi equiv_rel,
    2.15     equiv_thm = Morphism.thm phi equiv_thm}
    2.16  
    2.17 -fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str
    2.18 -
    2.19 -fun quotdata_lookup thy str =
    2.20 -  case Symtab.lookup (QuotData.get thy) str of
    2.21 -    SOME qinfo => qinfo
    2.22 -  | NONE => raise NotFound
    2.23 +fun quotdata_lookup thy str = Symtab.lookup (QuotData.get thy) str
    2.24  
    2.25  fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
    2.26  fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I

     3.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 07:48:07 2011 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:50:54 2011 +0200
     3.3 @@ -100,13 +100,9 @@
     3.4     a quotient definition
     3.5  *)
     3.6  fun get_rty_qty ctxt s =
     3.7 -  let
     3.8 -    val thy = Proof_Context.theory_of ctxt
     3.9 -    val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound =>
    3.10 -      raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
    3.11 -  in
    3.12 -    (#rtyp qdata, #qtyp qdata)
    3.13 -  end
    3.14 +  case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
    3.15 +    SOME qdata => (#rtyp qdata, #qtyp qdata)
    3.16 +  | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.");
    3.17  
    3.18  (* takes two type-environments and looks
    3.19     up in both of them the variable v, which
    3.20 @@ -302,12 +298,9 @@
    3.21    end
    3.22  
    3.23  fun get_equiv_rel ctxt s =
    3.24 -  let
    3.25 -    val thy = Proof_Context.theory_of ctxt
    3.26 -  in
    3.27 -    #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound =>
    3.28 -      raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
    3.29 -  end
    3.30 +  case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
    3.31 +      SOME qdata => #equiv_rel qdata
    3.32 +    | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
    3.33  
    3.34  fun equiv_match_err ctxt ty_pat ty =
    3.35    let
    3.36 @@ -442,7 +435,7 @@
    3.37            if length rtys <> length qtys then false
    3.38            else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
    3.39          else
    3.40 -          (case Quotient_Info.quotdata_lookup_raw thy qs of
    3.41 +          (case Quotient_Info.quotdata_lookup thy qs of
    3.42              SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
    3.43            | NONE => false)
    3.44      | _ => false)