--- a/Nominal/NewParser.thy	Tue Aug 17 07:11:45 2010 +0800
+++ b/Nominal/NewParser.thy	Tue Aug 17 17:52:25 2010 +0800
@@ -312,13 +312,15 @@
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
-  val raw_constrs = 
-    flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts))
+
   val raw_tys = all_dtyps descr sorts
   val raw_full_ty_names = map (fst o dest_Type) raw_tys
   
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names  
  
+  val raw_cns_info = all_dtyp_constrs_types descr sorts
+  val raw_constrs = flat (map (map (fn (c, _, _, _) => c)) raw_cns_info)
+
   val raw_inject_thms = flat (map #inject dtinfos)
   val raw_distinct_thms = flat (map #distinct dtinfos)
   val raw_induct_thm = #induct dtinfo
@@ -349,14 +351,15 @@
 
   val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = 
     if get_STEPS lthy3a > 3 
-    then define_raw_fvs descr sorts raw_bn_info raw_bclauses (raw_inject_thms @ raw_distinct_thms) lthy3a
+    then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses 
+      (raw_inject_thms @ raw_distinct_thms) lthy3a
     else raise TEST lthy3a
 
   (* definition of raw alphas *)
   val _ = warning "Definition of alphas";
   val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
     if get_STEPS lthy3b > 4 
-    then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b
+    then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3b
     else raise TEST lthy3b
   val alpha_tys = map (domain_type o fastype_of) alpha_trms