1.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 07:48:07 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 13:50:54 2011 +0200
     1.3 @@ -20,8 +20,7 @@
     1.4  
     1.5    type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
     1.6    val transform_quotdata: morphism -> quotdata_info -> quotdata_info
     1.7 -  val quotdata_lookup_raw: theory -> string -> quotdata_info option
     1.8 -  val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
     1.9 +  val quotdata_lookup: theory -> string -> quotdata_info option
    1.10    val quotdata_update_thy: string -> quotdata_info -> theory -> theory
    1.11    val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
    1.12    val quotdata_dest: Proof.context -> quotdata_info list
    1.13 @@ -136,12 +135,7 @@
    1.14     equiv_rel = Morphism.term phi equiv_rel,
    1.15     equiv_thm = Morphism.thm phi equiv_thm}
    1.16  
    1.17 -fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str
    1.18 -
    1.19 -fun quotdata_lookup thy str =
    1.20 -  case Symtab.lookup (QuotData.get thy) str of
    1.21 -    SOME qinfo => qinfo
    1.22 -  | NONE => raise NotFound
    1.23 +fun quotdata_lookup thy str = Symtab.lookup (QuotData.get thy) str
    1.24  
    1.25  fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
    1.26  fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I