39   programming on which @{ML \<open>apply\<close> in Timeout} relies.

    39   programming on which @{ML \<open>apply\<close> in Timeout} relies.

    40 

    40 

    41 \begin{readmore}

    41 \begin{readmore}

    42    The function @{ML \<open>apply\<close> in Timeout} is defined in the structure

    42    The function @{ML \<open>apply\<close> in Timeout} is defined in the structure

    43   @{ML_structure Timeout} which can be found in the file 

    43   @{ML_structure Timeout} which can be found in the file 

    45 \end{readmore}

    45 \end{readmore}

    46 

    46 

    47  

    47  

    48 \<close>

    48 \<close>

    49 end

    49 end