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

--- a/Nominal/Parser.thy	Sat Mar 27 12:26:59 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 27 13:50:59 2010 +0100
@@ -353,7 +353,6 @@
   val distincts = flat (map #distinct dtinfos);
   val rel_distinct = map #distinct rel_dtinfos;
   val induct = #induct dtinfo;
-  val inducts = #inducts dtinfo;
   val exhausts = map #exhaust dtinfos;
   val _ = tracing "Defining permutations, fv and alpha";
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
@@ -391,9 +390,7 @@
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
-  val lthy7 = define_quotient_type
-    (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn))
-    (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
+  val (q_tys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>
@@ -401,10 +398,9 @@
         Const (cname, map (typ_of_dtyp descr sorts) dts --->
           typ_of_dtyp descr sorts (DtRec i))) l) descr);
   val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7;
-  (* Could be done nicer *)
-  val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts);
   val _ = tracing "Proving respects";
   val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
+  val _ = map tracing (map PolyML.makestring bns_rsp_pre')
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ =>
        resolve_tac bns_rsp_pre' 1)) bns lthy8;

--- a/Nominal/Rsp.thy	Sat Mar 27 12:26:59 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 27 13:50:59 2010 +0100
@@ -94,8 +94,6 @@
 in
   Const (@{const_name permute}, @{typ perm} --> ty --> ty)
 end
-
-val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
 *}
 
 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"