diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Library/NatPair.thy
--- a/src/HOL/Library/NatPair.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/NatPair.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -16,7 +16,7 @@
 *}
 
 definition
-  nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
+  nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where
   "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
 
 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"