src/HOL/Tools/Function/fun.ML
changeset 43329 84472e198515
parent 43323 28e71a685c84
child 44237 2a2040c9d898
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Wed Jun 08 22:16:21 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Thu Jun 09 20:22:22 2011 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4          val (argTs, rT) = chop n (binder_types fT)
     1.5            |> apsnd (fn Ts => Ts ---> body_type fT)
     1.6  
     1.7 -        val qs = map Free (Name.invents Name.context "a" n ~~ argTs)
     1.8 +        val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
     1.9        in
    1.10          HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
    1.11            Const ("HOL.undefined", rT))