diff -r 114da911bc41 -r 9178a7f4c4c8 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Apr 07 21:25:22 2008 +0200
+++ b/src/Pure/Pure.thy	Mon Apr 07 21:29:46 2008 +0200
@@ -21,7 +21,7 @@
 lemmas meta_allE = meta_spec [elim_format]
 
 lemma swap_params:
-  "(\<And>x y. PROP P(x, y)) == (\<And>y x. PROP P(x, y))" ..
+  "(!!x y. PROP P(x, y)) == (!!y x. PROP P(x, y))" ..
 
 
 subsection {* Embedded terms *}
@@ -42,7 +42,7 @@
   shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
 proof
   assume conj: "!!x. PROP A(x) && PROP B(x)"
-  show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
+  show "(!!x. PROP A(x)) && (!!x. PROP B(x))"
   proof -
     fix x
     from conj show "PROP A(x)" by (rule conjunctionD1)