diff -r 1ad3159323dc -r 4877c4e184e5 src/FOL/ex/Nat_Class.thy
--- a/src/FOL/ex/Nat_Class.thy	Tue Aug 30 17:53:03 2011 +0200
+++ b/src/FOL/ex/Nat_Class.thy	Tue Aug 30 18:12:48 2011 +0200
@@ -26,9 +26,8 @@
     and rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
 begin
 
-definition
-  add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 60) where
-  "m + n = rec(m, n, \<lambda>x y. Suc(y))"
+definition add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 60)
+  where "m + n = rec(m, n, \<lambda>x y. Suc(y))"
 
 lemma Suc_n_not_n: "Suc(k) \<noteq> (k::'a)"
   apply (rule_tac n = k in induct)