src/HOL/Isar_examples/BasicLogic.thy

--- a/src/HOL/Isar_examples/BasicLogic.thy	Thu Jul 01 21:28:49 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Thu Jul 01 21:29:53 1999 +0200
@@ -106,7 +106,7 @@
   proof (rule exE);
     fix a;
     assume "P(f(a))" (is "P(??witness)");
-    show ??thesis; by (rule exI [with P ??witness]);
+    show ??thesis; by (rule exI [of P ??witness]);
   qed;
 qed;