src/HOL/HOLCF/Tools/fixrec.ML
changeset 43324 2b47822868e4
parent 42361 23f352990944
child 44080 53d95b52954c
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -234,7 +234,7 @@
     1.4            in comp_con T f rhs' (v::vs) taken' end
     1.5        | Const (c, cT) =>
     1.6            let
     1.7 -            val n = Name.variant taken "v"
     1.8 +            val n = singleton (Name.variant_list taken) "v"
     1.9              val v = Free(n, T)
    1.10              val m = Const(match_name c, matcherT (cT, fastype_of rhs))
    1.11              val k = big_lambdas vs rhs