--- a/Nominal/Nominal2.thy	Wed Jan 05 17:33:43 2011 +0000
+++ b/Nominal/Nominal2.thy	Thu Jan 06 11:00:16 2011 +0000
@@ -18,8 +18,6 @@
 use "nominal_dt_quot.ML"
 ML {* open Nominal_Dt_Quot *}
 
-
-
 (*****************************************)
 (* setup for induction principles method *)
 use "nominal_induct.ML"
@@ -75,11 +73,11 @@
 
 fun raw_dts ty_ss dts =
 let
-  fun raw_dts_aux1 (bind, tys, mx) =
-    (raw_bind bind, map (replace_typ ty_ss) tys, mx)
+  fun raw_dts_aux1 (bind, tys, _) =
+    (raw_bind bind, map (replace_typ ty_ss) tys, NoSyn)
 
-  fun raw_dts_aux2 (ty_args, bind, mx, constrs) =
-    (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs)
+  fun raw_dts_aux2 (ty_args, bind, _, constrs) =
+    (ty_args, raw_bind bind, NoSyn, map raw_dts_aux1 constrs)
 in
   map raw_dts_aux2 dts
 end
@@ -105,8 +103,8 @@
 ML {*
 fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs =
 let
-  val bn_funs' = map (fn (bn, ty, mx) => 
-    (raw_bind bn, SOME (replace_typ dts_env ty), mx)) bn_funs
+  val bn_funs' = map (fn (bn, ty, _) => 
+    (raw_bind bn, SOME (replace_typ dts_env ty), NoSyn)) bn_funs
   
   val bn_eqs' = map (fn (attr, trm) => 
     (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs
@@ -156,6 +154,8 @@
   val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs 
   val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses 
 
+  val _ = tracing ("raw_dt info:\n" ^ @{make_string} raw_dts)
+
   val (raw_dt_full_names, thy1) = 
     Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy