# HG changeset patch
# User haftmann
# Date 1254074304 -7200
# Node ID becd87e4039bf851004f42a9d9f50c0dcae4dff6
# Parent  32b97ef44ccd328f778cbdb27ad443dded59552e
adjusted to changes in datatype package

diff -r 32b97ef44ccd -r becd87e4039b src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun Sep 27 10:05:17 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Sep 27 19:58:24 2009 +0200
@@ -245,7 +245,7 @@
     val (full_new_type_names',thy1) =
       Datatype.add_datatype config new_type_names' dts'' thy;
 
-    val {descr, induction, ...} =
+    val {descr, inducts = (_, induct), ...} =
       Datatype.the_info thy1 (hd full_new_type_names');
     fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
@@ -322,7 +322,7 @@
                  Const ("Nominal.perm", T) $ pi $ Free (x, T2))
                end)
              (perm_names_types ~~ perm_indnames))))
-          (fn _ => EVERY [indtac induction perm_indnames 1,
+          (fn _ => EVERY [indtac induct perm_indnames 1,
             ALLGOALS (asm_full_simp_tac
               (global_simpset_of thy2 addsimps [perm_fun_def]))])),
         length new_type_names));
@@ -343,7 +343,7 @@
                    Free (x, T)))
                (perm_names ~~
                 map body_type perm_types ~~ perm_indnames)))))
-          (fn _ => EVERY [indtac induction perm_indnames 1,
+          (fn _ => EVERY [indtac induct perm_indnames 1,
             ALLGOALS (asm_full_simp_tac (global_simpset_of thy2))])),
         length new_type_names))
       end)
@@ -378,7 +378,7 @@
                     end)
                   (perm_names ~~
                    map body_type perm_types ~~ perm_indnames)))))
-           (fn _ => EVERY [indtac induction perm_indnames 1,
+           (fn _ => EVERY [indtac induct perm_indnames 1,
               ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
          length new_type_names)
       end) atoms);
@@ -414,7 +414,7 @@
                     end)
                   (perm_names ~~
                    map body_type perm_types ~~ perm_indnames))))))
-           (fn _ => EVERY [indtac induction perm_indnames 1,
+           (fn _ => EVERY [indtac induct perm_indnames 1,
               ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
          length new_type_names)
       end) atoms);
@@ -466,7 +466,7 @@
                      perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
                   end)
                 (perm_names ~~ Ts ~~ perm_indnames)))))
-          (fn _ => EVERY [indtac induction perm_indnames 1,
+          (fn _ => EVERY [indtac induct perm_indnames 1,
              ALLGOALS (asm_full_simp_tac simps)]))
       in
         fold (fn (s, tvs) => fn thy => AxClass.prove_arity