diff -r f4815812665b -r e61b058d58d2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Nat.thy	Fri Mar 24 12:30:35 1995 +0100
@@ -59,9 +59,9 @@
   (*nat operations and recursion*)
   nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  \
 \                                        & (!x. n=Suc(x) --> z=f(x))"
-  pred_nat_def  "pred_nat == {p. ? n. p = <n, Suc(n)>}"
+  pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
 
-  less_def "m<n == <m,n>:trancl(pred_nat)"
+  less_def "m<n == (m,n):trancl(pred_nat)"
 
   le_def   "m<=(n::nat) == ~(n<m)"