--- a/Nominal/Lift.thy	Thu Jun 24 00:41:41 2010 +0100
+++ b/Nominal/Lift.thy	Thu Jun 24 19:32:33 2010 +0100
@@ -11,11 +11,8 @@
   fun def_ty ((b, ty), (alpha, equivp)) ctxt =
     Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha, false)), equivp) ctxt;
   val alpha_equivps = List.take (equivps, length alphas)
-  val (thms, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt;
-  val quot_thms = map fst thms;
-  val quots = map (HOLogic.dest_Trueprop o prop_of) quot_thms;
-  val reps = map (hd o rev o snd o strip_comb) quots;
-  val qtys = map (domain_type o fastype_of) reps;
+  val (qinfo, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt;
+  val qtys = map #qtyp qinfo;
 in
   (qtys, ctxt')
 end

--- a/Nominal/Perm.thy	Thu Jun 24 00:41:41 2010 +0100
+++ b/Nominal/Perm.thy	Thu Jun 24 19:32:33 2010 +0100
@@ -24,8 +24,8 @@
 ML {*
 fun quotient_lift_consts_export qtys spec ctxt =
 let
-  val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
-  val (ts_loc, defs_loc) = split_list result;
+  val (result, ctxt') = fold_map (Quotient_Def.lift_raw_const qtys) spec ctxt;
+  val (ts_loc, defs_loc) = split_list (map (fn info => (#qconst info, #def info)) result);
   val morphism = ProofContext.export_morphism ctxt' ctxt;
   val ts = map (Morphism.term morphism) ts_loc
   val defs = Morphism.fact morphism defs_loc

--- a/Nominal/Rsp.thy	Thu Jun 24 00:41:41 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Jun 24 19:32:33 2010 +0100
@@ -5,7 +5,7 @@
 ML {*
 fun const_rsp qtys lthy const =
 let
-  val nty = fastype_of (Quotient_Term.quotient_lift_const qtys ("", const) lthy)
+  val nty = Quotient_Term.derive_qtyp qtys (fastype_of const) lthy
   val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
 in
   HOLogic.mk_Trueprop (rel $ const $ const)