--- a/Nominal/Ex/SingleLet.thy	Sun Jun 27 21:41:21 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Mon Jun 28 15:23:56 2010 +0100
@@ -4,7 +4,7 @@
 
 atom_decl name
 
-declare [[STEPS = 15]]
+declare [[STEPS = 16]]
 
 nominal_datatype trm  =
   Var "name"
@@ -21,6 +21,11 @@
 where
   "bn (As x y t) = {atom x}"
 
+term Var 
+term App
+term Baz
+
+
 typ trm
 typ assg
 

--- a/Nominal/NewParser.thy	Sun Jun 27 21:41:21 2010 +0100
+++ b/Nominal/NewParser.thy	Mon Jun 28 15:23:56 2010 +0100
@@ -72,21 +72,6 @@
 *}
 
 
-ML {* 
-(* exports back the results *)
-fun add_primrec_wrapper funs eqs lthy = 
-  if null funs then ([], [], lthy)
-  else 
-   let 
-     val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs
-     val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs
-     val ((funs'', eqs''), lthy') = Primrec.add_primrec funs' eqs' lthy
-     val phi = ProofContext.export_morphism lthy' lthy
-   in 
-     (map (Morphism.term phi) funs'', map (Morphism.thm phi) eqs'', lthy')
-   end
-*}
-
 ML {*
 fun add_datatype_wrapper dt_names dts =
 let
@@ -450,16 +435,25 @@
     else raise TEST lthy6
 
   val qtys = map #qtyp qty_infos
- 
+  val qconstr_descrs = 
+    flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts)
+    |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs
+
+  val (qconstrs, lthy8) = 
+    if get_STEPS lthy > 15
+    then qconst_defs qtys qconstr_descrs lthy7
+    else raise TEST lthy7
+
+  (* HERE *)
+
   val _ = tracing ("all_raw_tys: " ^ commas (map @{make_string} all_raw_tys))
   val _ = tracing ("constrs: " ^ commas (map @{make_string} all_raw_constrs))
   val _ = tracing ("qtys: " ^ commas (map @{make_string} qtys))
-  
+  val _ = tracing ("qconstrs " ^ commas (map @{make_string} qconstrs))
   
-
   val _ = 
-    if get_STEPS lthy > 15
-    then true else raise TEST lthy7
+    if get_STEPS lthy > 16
+    then true else raise TEST lthy8
   
   (* old stuff *)
 
@@ -470,7 +464,7 @@
         Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
           Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) const_names raw_consts
-  val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys dd lthy7;
+  val (consts, _, lthy8) = quotient_lift_consts_export qtys dd lthy7;
   val _ = warning "Proving respects";
 
   val bn_nos = map (fn (_, i, _) => i) raw_bn_info;

--- a/Nominal/nominal_dt_quot.ML	Sun Jun 27 21:41:21 2010 +0100
+++ b/Nominal/nominal_dt_quot.ML	Mon Jun 28 15:23:56 2010 +0100
@@ -26,10 +26,12 @@
   fold_map Quotient_Type.add_quotient_type qty_args2 lthy
 end 
 
+
 (* defines quotient constants *)
-fun qconst_defs qtys const_spec lthy =
+fun qconst_defs qtys consts_specs lthy =
 let
-  val (qconst_infos, lthy') = fold_map (Quotient_Def.lift_raw_const qtys) const_spec lthy
+  val (qconst_infos, lthy') = 
+    fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy
   val phi = ProofContext.export_morphism lthy' lthy
 in
   (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy')