781   The positional information is stored as part of an XML-tree so that code 

   781   The positional information is stored as part of an XML-tree so that code 

   782   called later on will be able to give more precise error messages. 

   782   called later on will be able to give more precise error messages. 

   783 

   783 

   784   \begin{readmore}

   784   \begin{readmore}

   785   The functions to do with input and output of XML and YXML are defined 

   785   The functions to do with input and output of XML and YXML are defined 

   787   \end{readmore}

   787   \end{readmore}

   788   

   788   

   789   FIXME:

   789   FIXME:

   790   @{ML_ind parse_term in Syntax} @{ML_ind check_term in Syntax}

   790   @{ML_ind parse_term in Syntax} @{ML_ind check_term in Syntax}

   791   @{ML_ind parse_typ in Syntax} @{ML_ind check_typ in Syntax}

   791   @{ML_ind parse_typ in Syntax} @{ML_ind check_typ in Syntax}