diff -r 6613514ff6cb -r cfc795473656 Nominal/nominal_dt_rawfuns.ML
--- 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)