diff -r 8279a25ad0ae -r 9460a4cf0acc src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed Mar 28 19:16:11 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Wed Mar 28 19:17:40 2007 +0200
@@ -1137,8 +1137,8 @@
  
     val (_, thy9) = thy8 |>
       Theory.add_path big_name |>
-      PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] ||>>
-      PureThy.add_thmss [(("inducts_weak", projections dt_induct), [case_names_induct])] ||>
+      PureThy.add_thms [(("weak_induct", dt_induct), [case_names_induct])] ||>>
+      PureThy.add_thmss [(("weak_inducts", projections dt_induct), [case_names_induct])] ||>
       Theory.parent_path ||>>
       DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
       DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>