doc-src/Tutorial/Misc/exorproof.ML

- Inserted additional check for equality types in check_mode_clause that
avoids ill-typed code to be generated.
- Mode inference algorithm now outputs additional diagnostic messages.

by(simp_tac (simpset() addsimps [exor_def]) 1);