Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/method.ML
changeset 14508 859b11514537
parent 14215 ebf291f3b449
child 14718 f52f2cf2d137 
--- 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)
isabelle