--- a/Nominal/Lift.thy	Sat Mar 27 12:26:59 2010 +0100
+++ b/Nominal/Lift.thy	Sat Mar 27 13:50:59 2010 +0100
@@ -2,14 +2,20 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"
 begin
 
+
 ML {*
-fun define_quotient_type args tac ctxt =
+fun define_quotient_types binds tys alphas equivps ctxt =
 let
-  val mthd = Method.SIMPLE_METHOD tac
-  val mthdt = Method.Basic (fn _ => mthd)
-  val bymt = Proof.global_terminal_proof (mthdt, NONE)
+  fun def_ty ((b, ty), (alpha, equivp)) ctxt =
+    Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha)), 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;
 in
-  bymt (Quotient_Type.quotient_type args ctxt)
+  (qtys, ctxt')
 end
 *}