local 
    exception negativeInteger

    fun factorial_tr (n, p) = 
	(* INV: n_0 >= 0 /\ n_0! = n!*p *)
	if n = 0 then p
	else factorial_tr (n-1, n*p)

in fun factorial n =
       if n < 0 then raise negativeInteger
       else factorial_tr (n, 1)
end