TFL/tfl.ML
changeset 12902 a23dc0b7566f
parent 11632 6fc8de600f58
child 14217 9f5679e97eac
equal deleted inserted replaced
12901:4570584fbda9 12902:a23dc0b7566f
    80 fun gvvariant names =
    80 fun gvvariant names =
    81   let val slist = ref names
    81   let val slist = ref names
    82       val vname = ref "u"
    82       val vname = ref "u"
    83       fun new() =
    83       fun new() =
    84          if !vname mem_string (!slist)
    84          if !vname mem_string (!slist)
    85          then (vname := bump_string (!vname);  new())
    85          then (vname := Symbol.bump_string (!vname);  new())
    86          else (slist := !vname :: !slist;  !vname)
    86          else (slist := !vname :: !slist;  !vname)
    87   in
    87   in
    88   fn ty => Free(new(), ty)
    88   fn ty => Free(new(), ty)
    89   end;
    89   end;
    90 
    90