--- a/Nominal/Ex/CoreHaskell.thy	Thu Jun 24 19:32:33 2010 +0100
+++ b/Nominal/Ex/CoreHaskell.thy	Thu Jun 24 21:35:11 2010 +0100
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 14]]
+declare [[STEPS = 15]]
 
 nominal_datatype tkind =
   KStar
@@ -85,7 +85,6 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
-
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm

--- a/Nominal/Ex/SingleLet.thy	Thu Jun 24 19:32:33 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Thu Jun 24 21:35:11 2010 +0100
@@ -4,9 +4,9 @@
 
 atom_decl name
 
-declare [[STEPS = 14]]
+declare [[STEPS = 15]]
 
-nominal_datatype trm =
+nominal_datatype trm  =
   Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind_set x in t
@@ -21,6 +21,9 @@
 where
   "bn (As x y t) = {atom x}"
 
+typ trm
+typ assg
+
 thm trm_assg.fv
 thm trm_assg.supp
 thm trm_assg.eq_iff

--- a/Nominal/NewParser.thy	Thu Jun 24 19:32:33 2010 +0100
+++ b/Nominal/NewParser.thy	Thu Jun 24 21:35:11 2010 +0100
@@ -366,7 +366,8 @@
     if get_STEPS lthy3b > 4 
     then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b
     else raise TEST lthy3b
-  
+  val alpha_tys = map (domain_type o fastype_of) alpha_trms  
+
   (* definition of alpha-distinct lemmas *)
   val _ = warning "Distinct theorems";
   val (alpha_distincts, alpha_bn_distincts) = 
@@ -396,11 +397,11 @@
        (Local_Theory.restore lthy_tmp)
     else raise TEST lthy4
  
-  val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
+  val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
 
-  val (alpha_eqvt, lthy_tmp'') =
+  val (alpha_eqvt, lthy6) =
     if get_STEPS lthy > 8
-    then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy_tmp'
+    then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
     else raise TEST lthy4
 
   (* proving alpha equivalence *)
@@ -408,51 +409,56 @@
 
   val alpha_refl_thms = 
     if get_STEPS lthy > 9
-    then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy_tmp'' 
-    else raise TEST lthy4
+    then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy6 
+    else raise TEST lthy6
 
   val alpha_sym_thms = 
     if get_STEPS lthy > 10
-    then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy_tmp'' 
-    else raise TEST lthy4
+    then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6 
+    else raise TEST lthy6
 
   val alpha_trans_thms = 
     if get_STEPS lthy > 11
     then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) 
-           alpha_intros alpha_induct alpha_cases lthy_tmp'' 
-    else raise TEST lthy4
+           alpha_intros alpha_induct alpha_cases lthy6
+    else raise TEST lthy6
 
   val alpha_equivp_thms = 
     if get_STEPS lthy > 12
-    then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy_tmp''
-    else raise TEST lthy4
+    then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy6
+    else raise TEST lthy6
 
   (* proving alpha implies alpha_bn *)
   val _ = warning "Proving alpha implies bn"
 
   val alpha_bn_imp_thms = 
     if get_STEPS lthy > 13
-    then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy_tmp'' 
-    else raise TEST lthy4
+    then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 
+    else raise TEST lthy6
   
-  val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms))
-  val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms))
-  val _ = tracing ("alpha_refl\n" ^ 
-    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms))
-  val _ = tracing ("alpha_bn_imp\n" ^ 
-    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms))
-  val _ = tracing ("alpha_equivp\n" ^ 
-    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_equivp_thms))
-
-  (* old stuff *)
-  val _ = 
-    if get_STEPS lthy > 14
-    then true else raise TEST lthy4
-
-  val qty_binds = map (fn (_, b, _, _) => b) dts;
+  (* defining the quotient type *)
+  val _ = warning "Declaring the quotient types"
+  val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
+  val qty_binds = map (fn (_, bind, _, _) => bind) dts
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
-  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp_thms lthy4;
+  
+  val qty_args' = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
+  val qty_args = (qty_descr ~~ qty_args') ~~ alpha_equivp_thms 
+ 
+  val (qty_infos, lthy7) = 
+    if get_STEPS lthy > 14
+    then fold_map Quotient_Type.add_quotient_type qty_args lthy6
+    else raise TEST lthy6
+
+  val qtys = map #qtyp qty_infos
+
+  val _ = 
+    if get_STEPS lthy > 15
+    then true else raise TEST lthy7
+  
+  (* old stuff *)
+
   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)) =>