Replaced arbitrary by undefined.
authorberghofe
Fri Oct 31 10:35:30 2008 +0100 (2008-10-31)
changeset 2871160e51a045755
parent 28710 e2064974c114
child 28712 4f2954d995f0
Replaced arbitrary by undefined.
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Thu Oct 30 10:57:45 2008 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Oct 31 10:35:30 2008 +0100
     1.3 @@ -539,7 +539,7 @@
     1.4             let val p as (y, _) = bG i
     1.5             in (tab := (x, p) :: !tab; y) end
     1.6         | SOME (y, _) => y,
     1.7 -     fn () => Basics.fold mk_upd (!tab) (Const ("arbitrary", aT --> bT)))
     1.8 +     fn () => Basics.fold mk_upd (!tab) (Const ("HOL.undefined", aT --> bT)))
     1.9    end;
    1.10  *}
    1.11