diff -r e129fcc720c1 -r 3e3c2af5e8a5 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Dec 19 16:41:55 2012 +0100
+++ b/src/Pure/Pure.thy	Wed Dec 19 22:26:26 2012 +0100
@@ -146,7 +146,7 @@
 qed
 
 lemma imp_conjunction:
-  "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
+  "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
 proof
   assume conj: "PROP A ==> PROP B &&& PROP C"
   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"