--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Apr 18 17:33:11 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Apr 18 17:33:11 2012 +0100
@@ -27,10 +27,7 @@
text "... and display nicely."
ML {*
- List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas;
-
- (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
- List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
+ List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #3) fmlas;
*}
subsection "Multiple tests"