1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -326,7 +326,7 @@
     1.4    (case AList.lookup (op =) vs s of
     1.5      NONE => (s, (names, (s, [s])::vs))
     1.6    | SOME xs =>
     1.7 -      let val s' = Name.variant names s
     1.8 +      let val s' = singleton (Name.variant_list names) s
     1.9        in (s', (s'::names, AList.update (op =) (s, s'::xs) vs)) end);
    1.10  
    1.11  fun distinct_v (Var ((s, 0), T)) nvs =
    1.12 @@ -414,7 +414,7 @@
    1.13      fun check_constrt t (names, eqs) =
    1.14        if is_constrt thy t then (t, (names, eqs))
    1.15        else
    1.16 -        let val s = Name.variant names "x";
    1.17 +        let val s = singleton (Name.variant_list names) "x";
    1.18          in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end;
    1.19  
    1.20      fun compile_eq (s, t) gr =