1012   in

  1012   in

  1013     map (fst o dest_Const o snd o dest_term) def_terms

  1013     map (fst o dest_Const o snd o dest_term) def_terms

  1014   end

  1014   end

  1015 *}

  1015 *}

  1016 

  1016 

  1017 ML {*

  1018 ML {*

  1018 fun lift_thm lthy qty qty_name rsp_thms defs t = let

  1019 fun lift_thm lthy qty qty_name rsp_thms defs t = let

  1019   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;

  1020   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;

  1020   val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;

  1021   val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;

  1021   val consts = lookup_quot_consts defs;

  1022   val consts = lookup_quot_consts defs;