src/Tools/eqsubst.ML
changeset 43324 2b47822868e4
parent 41164 6854e9a40edc
child 44095 3ea5fae095dc
     1.1 --- a/src/Tools/eqsubst.ML	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -179,7 +179,7 @@
     1.4  fun fakefree_badbounds Ts t = 
     1.5      let val (FakeTs,Ts,newnames) = 
     1.6              List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
     1.7 -                           let val newname = Name.variant usednames n
     1.8 +                           let val newname = singleton (Name.variant_list usednames) n
     1.9                             in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
    1.10                                 (newname,ty)::Ts, 
    1.11                                 newname::usednames) end)