src/HOL/Tools/Function/fun.ML
changeset 56254 a2dd9200854d
parent 54407 e95831757903
child 58826 2ed2eaabe3df
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -73,7 +73,7 @@
     1.4          val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
     1.5        in
     1.6          HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
     1.7 -          Const ("HOL.undefined", rT))
     1.8 +          Const (@{const_name undefined}, rT))
     1.9          |> HOLogic.mk_Trueprop
    1.10          |> fold_rev Logic.all qs
    1.11        end