src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Thu Oct 30 10:57:45 2008 +0100
+++ b/src/HOL/Fun.thy	Fri Oct 31 10:35:30 2008 +0100
@@ -539,7 +539,7 @@
            let val p as (y, _) = bG i
            in (tab := (x, p) :: !tab; y) end
        | SOME (y, _) => y,
-     fn () => Basics.fold mk_upd (!tab) (Const ("arbitrary", aT --> bT)))
+     fn () => Basics.fold mk_upd (!tab) (Const ("HOL.undefined", aT --> bT)))
   end;
 *}