--- a/src/HOL/Nat.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Nat.thy Fri Feb 14 07:53:46 2014 +0100
@@ -82,7 +82,7 @@
apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
done
-wrap_free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
+free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
apply atomize_elim
apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
@@ -101,7 +101,7 @@
setup {* Sign.parent_path *}
--- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+-- {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
setup {* Sign.mandatory_path "nat" *}
declare