diff -r e3f04fdd994d -r ed3a58a9eae1 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun May 18 17:03:20 2008 +0200
+++ b/src/Pure/Pure.thy	Sun May 18 17:03:23 2008 +0200
@@ -14,14 +14,14 @@
 lemmas meta_impE = meta_mp [elim_format]
 
 lemma meta_spec:
-  assumes "!!x. PROP P(x)"
-  shows "PROP P(x)"
-    by (rule `!!x. PROP P(x)`)
+  assumes "!!x. PROP P x"
+  shows "PROP P x"
+    by (rule `!!x. PROP P x`)
 
 lemmas meta_allE = meta_spec [elim_format]
 
 lemma swap_params:
-  "(!!x y. PROP P(x, y)) == (!!y x. PROP P(x, y))" ..
+  "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
 
 
 subsection {* Embedded terms *}
@@ -39,22 +39,22 @@
 
 lemma all_conjunction:
   includes meta_conjunction_syntax
-  shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
+  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 "(!!x. PROP A(x)) && (!!x. PROP B(x))"
+  assume conj: "!!x. PROP A 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)
-    from conj show "PROP B(x)" by (rule conjunctionD2)
+    from conj show "PROP A x" by (rule conjunctionD1)
+    from conj show "PROP B x" by (rule conjunctionD2)
   qed
 next
-  assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
+  assume conj: "(!!x. PROP A x) && (!!x. PROP B x)"
   fix x
-  show "PROP A(x) && PROP B(x)"
+  show "PROP A x && PROP B x"
   proof -
-    show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
-    show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
+    show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
+    show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
   qed
 qed