# HG changeset patch
# User berghofe
# Date 1175102260 -7200
# Node ID 9460a4cf0acc2a59fa39dee45ce3ba764026b736
# Parent  8279a25ad0ae49ae11616de229f170a54ef7a79d
Renamed induct(s)_weak to weak_induct(s) in order to unify
naming scheme with the one used in nominal_inductive.

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 ||>>