diff -r 0af3da3beae8 -r 859b11514537 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/method.ML	Fri Apr 02 14:08:30 2004 +0200
@@ -368,7 +368,8 @@
 	val params = Logic.strip_params Bi
 			     (* params of subgoal i as string typ pairs *)
 	val params = rev(Term.rename_wrt_term Bi params)
-						 (* as they are printed *)
+			   (* as they are printed: bound variables with *)
+                           (* the same name are renamed during printing *)
         fun types' (a, ~1) = (case assoc (params, a) of
                 None => types (a, ~1)
               | some => some)