# HG changeset patch
# User wenzelm
# Date 1434302131 -7200
# Node ID 4c65bd64bba43bc8efdf26da30fced98be4221bd
# Parent  7dc683911e5da7365f5941a66ba49925ce1b9cda
tuned comment;

diff -r 7dc683911e5d -r 4c65bd64bba4 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Jun 14 17:06:20 2015 +0100
+++ b/src/Pure/Isar/obtain.ML	Sun Jun 14 19:15:31 2015 +0200
@@ -132,11 +132,11 @@
 (** consider: generalized elimination and cases rule **)
 
 (*
-  consider x where (a) "A x" | y (b) where "B x" | ... ==
+  consider (a) x where "A x" | (b) y where "B y" | ... ==
 
   have thesis
     if a [intro?]: "!!x. A x ==> thesis"
-    and b [intro?]: "!!x. B x ==> thesis"
+    and b [intro?]: "!!y. B y ==> thesis"
     and ...
     for thesis
     apply (insert that)
@@ -287,9 +287,9 @@
   {
     fix thesis
     <chain_facts> have "PROP ?guess"
-      apply magic      -- {* turns goal into "thesis ==> #thesis" *}
+      apply magic      -- {* turn goal into "thesis ==> #thesis" *}
       <proof body>
-      apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into
+      apply_end magic  -- {* turn final "(!!x. P x ==> thesis) ==> #thesis" into
         "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
       <proof end>
   }