# HG changeset patch
# User urbanc
# Date 1130518406 -7200
# Node ID f6abeac6dcb5e77565e42bf1712c0769d9411b72
# Parent  8f3a80033ba4d3e0fc5a178e0fcfc94ed0ab9a1f
fixed case names in the weak induction principle and
changed name from "induct" to "induct_weak"

diff -r 8f3a80033ba4 -r f6abeac6dcb5 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Fri Oct 28 18:22:26 2005 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Oct 28 18:53:26 2005 +0200
@@ -1893,11 +1893,11 @@
             DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
                 (prems ~~ constr_defs))]));
 
-    val case_names_induct = mk_case_names_induct descr;
+    val case_names_induct = mk_case_names_induct (List.concat descr');
 
     val (thy9, _) = thy8 |>
       Theory.add_path big_name |>
-      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
+      PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] |>>
       Theory.parent_path |>>>
       DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>>
       DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>