doc-src/TutorialI/settings.ML

gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings

Thy_Output.indent_default := 5;