author | berghofe |
Fri, 31 Oct 2008 10:35:30 +0100 | |
changeset 28711 | 60e51a045755 |
parent 28710 | e2064974c114 |
child 28712 | 4f2954d995f0 |
src/HOL/Fun.thy | file | annotate | diff | comparison | revisions |
--- 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; *}