src/HOL/TPTP/TPTP_Interpret_Test.thy
changeset 47548 60849d8c457d
parent 47547 1a5dc8377b5c
child 47558 55b42f9af99d
     1.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Apr 18 17:33:11 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Apr 18 17:33:11 2012 +0100
     1.3 @@ -27,10 +27,7 @@
     1.4  
     1.5  text "... and display nicely."
     1.6  ML {*
     1.7 -  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas;
     1.8 -
     1.9 -  (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
    1.10 -  List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
    1.11 +  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #3) fmlas;
    1.12  *}
    1.13  
    1.14  subsection "Multiple tests"