Extended 'Define' to create recursive functions with high rank results.

Previously the system did not permit definitions like

- val _ = Datatype.Hol_datatype
     `D = i of (?'b. 'b -> 'b -> bool)
        | j of D`;

- val d_def = Define `(d (i e) = e) /\
                      (d (j a) = d a)`;

> val d_def =
    |- (!(e :?'b. 'b -> 'b -> bool). d (i e) = e) /\ !(a :D). d (j a) = d a
     : thm

because the result of calling "d" should be of rank 1, but the
normal function existence theorem (D_Axiom) can only handle
a result type of rank 0 ('a in the theorem below):

- theorem "D_Axiom";
> val it =
    |- !(f0 :(?'b. 'b -> 'b -> bool) -> 'a) (f1 :D -> 'a -> 'a).
         ?(fn :D -> 'a).
           (!(a :?'b. 'b -> 'b -> bool). fn (i a) = f0 a) /\
           !(a :D). fn (j a) = f1 a (fn a)
     : thm

But now the system can accept such definitions, because the type
database now has an entry for a function to fashion a function
existence theorem for a result type of any rank. In addition,
'Define' now uses this entry when needed to create a new recursive
function that can return a value of any required rank. No extra
input is needed from the user beyond the specification of the new
function, as above.