1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 07:48:07 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:50:54 2011 +0200
     1.3 @@ -100,13 +100,9 @@
     1.4     a quotient definition
     1.5  *)
     1.6  fun get_rty_qty ctxt s =
     1.7 -  let
     1.8 -    val thy = Proof_Context.theory_of ctxt
     1.9 -    val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound =>
    1.10 -      raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
    1.11 -  in
    1.12 -    (#rtyp qdata, #qtyp qdata)
    1.13 -  end
    1.14 +  case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
    1.15 +    SOME qdata => (#rtyp qdata, #qtyp qdata)
    1.16 +  | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.");
    1.17  
    1.18  (* takes two type-environments and looks
    1.19     up in both of them the variable v, which
    1.20 @@ -302,12 +298,9 @@
    1.21    end
    1.22  
    1.23  fun get_equiv_rel ctxt s =
    1.24 -  let
    1.25 -    val thy = Proof_Context.theory_of ctxt
    1.26 -  in
    1.27 -    #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound =>
    1.28 -      raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
    1.29 -  end
    1.30 +  case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of
    1.31 +      SOME qdata => #equiv_rel qdata
    1.32 +    | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
    1.33  
    1.34  fun equiv_match_err ctxt ty_pat ty =
    1.35    let
    1.36 @@ -442,7 +435,7 @@
    1.37            if length rtys <> length qtys then false
    1.38            else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
    1.39          else
    1.40 -          (case Quotient_Info.quotdata_lookup_raw thy qs of
    1.41 +          (case Quotient_Info.quotdata_lookup thy qs of
    1.42              SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
    1.43            | NONE => false)
    1.44      | _ => false)