1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:50:54 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:50:55 2011 +0200
     1.3 @@ -63,13 +63,9 @@
     1.4    | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
     1.5  
     1.6  fun get_mapfun ctxt s =
     1.7 -  let
     1.8 -    val thy = Proof_Context.theory_of ctxt
     1.9 -    val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
    1.10 -      raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    1.11 -  in
    1.12 -    Const (mapfun, dummyT)
    1.13 -  end
    1.14 +  case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
    1.15 +    SOME map_data => Const (#mapfun map_data, dummyT)
    1.16 +  | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    1.17  
    1.18  (* makes a Free out of a TVar *)
    1.19  fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
    1.20 @@ -275,13 +271,9 @@
    1.21    Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
    1.22  
    1.23  fun get_relmap ctxt s =
    1.24 -  let
    1.25 -    val thy = Proof_Context.theory_of ctxt
    1.26 -    val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
    1.27 -      raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
    1.28 -  in
    1.29 -    Const (relmap, dummyT)
    1.30 -  end
    1.31 +  case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
    1.32 +    SOME map_data => Const (#relmap map_data, dummyT)
    1.33 +  | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
    1.34  
    1.35  fun mk_relmap ctxt vs rty =
    1.36    let