1.1 --- a/doc-src/Ref/defining.tex	Wed Jan 18 11:36:04 1995 +0100
     1.2 +++ b/doc-src/Ref/defining.tex	Thu Jan 19 16:05:21 1995 +0100
     1.3 @@ -688,26 +688,10 @@
     1.4  {\out ...}
     1.5  \end{ttbox}
     1.6  
     1.7 -On the other hand it's also possible that none of the parse trees can be
     1.8 -typed correctly although the user did not make a mistake.
     1.9 -
    1.10 -%% FIXME remove?
    1.11 -%By default Isabelle
    1.12 -%assumes that the type of a syntax translation rule is {\tt logic} but does
    1.13 -%not look at the type unless parsing the rule produces more than one parse
    1.14 -%tree. In that case this message is output if the rule's type is different
    1.15 -%from {\tt logic}:
    1.16 -%
    1.17 -%\begin{ttbox}
    1.18 -%{\out Warning: Ambiguous input "..."}
    1.19 -%{\out produces the following parse trees:}
    1.20 -%{\out ...}
    1.21 -%{\out This occured in syntax translation rule: "..."  ->  "..."}
    1.22 -%{\out Type checking error: Term does not have expected type}
    1.23 -%{\out ...}
    1.24 -%\end{ttbox}
    1.25 -%
    1.26 -%To circumvent this the rule's type has to be stated.
    1.27 +Ambiguities occuring in syntax translation rules cannot be resolved by
    1.28 +type inference because it is not necessary for these rules to be type
    1.29 +correct. Therefore Isabelle always generates an error message and the
    1.30 +ambiguity should be eliminated by changing the grammar or the rule.
    1.31  
    1.32  
    1.33  \section{Example: some minimal logics} \label{sec:min_logics}