diff -r 6613514ff6cb -r cfc795473656 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Dec 05 17:05:56 2011 +0000
+++ b/Nominal/Nominal2.thy	Tue Dec 06 23:42:19 2011 +0000
@@ -109,13 +109,7 @@
 *}
 
 ML {*
-fun rawify_dts dt_names dts dts_env =
-let
-  val raw_dts = raw_dts dts_env dts
-  val raw_dt_names = add_raws dt_names
-in
-  (raw_dt_names, raw_dts)
-end 
+fun rawify_dts dts dts_env = raw_dts dts_env dts
 *}
 
 ML {*
@@ -168,12 +162,12 @@
   val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) 
     (bn_fun_strs ~~ bn_fun_strs')
   
-  val (raw_full_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
+  val raw_dts = rawify_dts dts dts_env
   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 (raw_full_dt_names', thy1) = 
-    Datatype.add_datatype Datatype.default_config raw_full_dt_names raw_dts thy
+    Datatype.add_datatype Datatype.default_config raw_dts thy
 
   val lthy1 = Named_Target.theory_init thy1