src/HOL/Tools/Function/fun.ML

--- a/src/HOL/Tools/Function/fun.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -73,7 +73,7 @@
         val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
       in
         HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
-          Const ("HOL.undefined", rT))
+          Const (@{const_name undefined}, rT))
         |> HOLogic.mk_Trueprop
         |> fold_rev Logic.all qs
       end