doc-src/TutorialI/Trie/ROOT.ML

fix parsing of higher-order formulas;
this code was never exercised before because the current ATPs perform clausification, but someday ATPs might support FOF natively

use "../settings.ML";
use_thy "Trie";