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