Boolean predicate to function

[Andre Renaud <ajr74@student.canterbury.ac.nz>]

I have a fairly simple PVS question. In my current encoding I have a lot
of functions defined in the form:

foo(a, b : nat) : bool =
...

These are generally a predicate which returns true if b is correct for
some a.
I have recently found the need to have these written in the following
style as well:

foo(a : nat): nat =
...

where I  now return the value of b. Is there a simple way to write the
second function given the first? I've tried the following, but it isn't
particularly successful:

foo_return(a : nat): nat = 
	FORALL(b : nat):
		if (foo(a, b)) then
			b
		else
			0
		endif

But I get the following error message:
Error: the assertion (COMPATIBLE? (TYPE LHS) (TYPE RHS)) failed


Thanks,
-- 
Andre Renaud
Computer Science Department, University of Canterbury