Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_dt_rawfuns.ML
changeset 3061 cfc795473656
parent 3045 d0ad264f8c4f
child 3065 51ef8a3cb6ef 
--- 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)
nominal2