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