1.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -101,7 +101,7 @@
     1.4        val names = usednames_of_thm rule;
     1.5        val (fromnames,tonames,names2,Ts') = 
     1.6            Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
     1.7 -                    let val n2 = Name.variant names n in
     1.8 +                    let val n2 = singleton (Name.variant_list names) n in
     1.9                        (ctermify (Free(faken,ty)) :: rnf,
    1.10                         ctermify (Free(n2,ty)) :: rnt, 
    1.11                         n2 :: names,
    1.12 @@ -146,7 +146,7 @@
    1.13        val vars_to_fix = union (op =) termvars cond_vs;
    1.14        val (renamings, names2) = 
    1.15            List.foldr (fn (((n,i),ty), (vs, names')) => 
    1.16 -                    let val n' = Name.variant names' n in
    1.17 +                    let val n' = singleton (Name.variant_list names') n in
    1.18                        ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
    1.19                      end)
    1.20                  ([], names) vars_to_fix;
    1.21 @@ -154,7 +154,7 @@
    1.22  
    1.23  (* make a new fresh typefree instantiation for the given tvar *)
    1.24  fun new_tfree (tv as (ix,sort), (pairs,used)) =
    1.25 -      let val v = Name.variant used (string_of_indexname ix)
    1.26 +      let val v = singleton (Name.variant_list used) (string_of_indexname ix)
    1.27        in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
    1.28  
    1.29