--- 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,9 @@
apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
done
-free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
+free_constructors case_nat for
+ =: "0 \<Colon> nat" (defaults pred: "0 \<Colon> nat")
+ | Suc pred
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