diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/Acc.ML
--- a/src/HOL/ex/Acc.ML	Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/Acc.ML	Fri Mar 24 12:30:35 1995 +0100
@@ -13,12 +13,12 @@
 
 (*The intended introduction rule*)
 val prems = goal Acc.thy
-    "[| !!b. <b,a>:r ==> b: acc(r) |] ==> a: acc(r)";
+    "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
 by (fast_tac (set_cs addIs (prems @ 
 			    map (rewrite_rule [pred_def]) acc.intrs)) 1);
 qed "accI";
 
-goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
+goal Acc.thy "!!a b r. [| b: acc(r);  (a,b): r |] ==> a: acc(r)";
 by (etac acc.elim 1);
 by (rewtac pred_def);
 by (fast_tac set_cs 1);
@@ -26,7 +26,7 @@
 
 val [major,indhyp] = goal Acc.thy
     "[| a : acc(r);						\
-\       !!x. [| x: acc(r);  ALL y. <y,x>:r --> P(y) |] ==> P(x)	\
+\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x)	\
 \    |] ==> P(a)";
 by (rtac (major RS acc.induct) 1);
 by (rtac indhyp 1);
@@ -44,7 +44,7 @@
 by (fast_tac set_cs 1);
 qed "acc_wfI";
 
-val [major] = goal Acc.thy "wf(r) ==> ALL x. <x,y>: r | <y,x>:r --> y: acc(r)";
+val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
 by (rtac (major RS wf_induct) 1);
 br (impI RS allI) 1;
 br accI 1;