src/Tools/IsaPlanner/isand.ML
changeset 43324 2b47822868e4
parent 35845 e5980f0ad025
child 44121 44adaa6db327
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4        val tvars = List.foldr OldTerm.add_term_tvars [] ts;
     1.5        val (names',renamings) = 
     1.6            List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
     1.7 -                         let val n2 = Name.variant Ns n in 
     1.8 +                         let val n2 = singleton (Name.variant_list Ns) n in 
     1.9                             (n2::Ns, (tv, (n2,s))::Rs)
    1.10                           end) (tfree_names @ names,[]) tvars;
    1.11      in renamings end;
    1.12 @@ -223,7 +223,7 @@
    1.13        val Ns = List.foldr OldTerm.add_term_names names ts;
    1.14        val (_,renamings) = 
    1.15            Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
    1.16 -                    let val n2 = Name.variant Ns n in
    1.17 +                    let val n2 = singleton (Name.variant_list Ns) n in
    1.18                        (n2 :: Ns, (v, (n2,ty)) :: Rs)
    1.19                      end) ((Ns,[]), vars);
    1.20      in renamings end;