--- 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