src/Pure/Isar/method.ML

     val Ts = map get_typ xis;
 	val (_, _, Bi, _) = dest_state(st,i)
 	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)
           | types' xi = types xi;
         val used = add_term_tvarnames