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