author | wenzelm |
Sun, 25 Sep 2005 23:36:14 +0200 | |
changeset 17642 | e063c0403650 |
parent 17641 | 5ec55c1fa116 |
child 17643 | 7e417a7cbf9f |
src/Pure/term.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/term.ML Sun Sep 25 20:24:23 2005 +0200 +++ b/src/Pure/term.ML Sun Sep 25 23:36:14 2005 +0200 @@ -1262,7 +1262,7 @@ fun zero_var_inst vars = fold (fn v as ((x, i), X) => fn (used, inst) => let - val x' = variant used x; + val x' = variant used (if is_bound x then "u" else x); val used' = x' :: used; in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end) vars ([], []) |> #2;