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

--- a/Nominal/nominal_dt_rawfuns.ML	Mon Dec 05 17:05:56 2011 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Dec 06 23:42:19 2011 +0000
@@ -358,7 +358,7 @@
 
     val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
 
-    val tac = (Datatype_Aux.indtac induct perm_indnames 
+    val tac = (Datatype_Aux.ind_tac induct perm_indnames 
                THEN_ALL_NEW asm_simp_tac simps) 1
   in
     Goal.prove lthy perm_indnames [] goals (K tac)
@@ -382,7 +382,7 @@
 
     val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
 
-    val tac = (Datatype_Aux.indtac induct perm_indnames
+    val tac = (Datatype_Aux.ind_tac induct perm_indnames
                THEN_ALL_NEW asm_simp_tac simps) 1
   in
     Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)