src/Pure/Pure.thy

--- a/src/Pure/Pure.thy	Fri May 11 00:43:46 2007 +0200
+++ b/src/Pure/Pure.thy	Fri May 11 01:07:10 2007 +0200
@@ -94,8 +94,11 @@
   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
 proof
   assume r: "PROP A && PROP B ==> PROP C"
-  assume "PROP A" and "PROP B"
-  show "PROP C" by (rule r) -
+  assume ab: "PROP A" "PROP B"
+  show "PROP C"
+  proof (rule r)
+    from ab show "PROP A && PROP B" .
+  qed
 next
   assume r: "PROP A ==> PROP B ==> PROP C"
   assume conj: "PROP A && PROP B"