# HG changeset patch # User sultana # Date 1378241201 -3600 # Node ID a1a45fdc53a3084d6e5662b8494183b7a26d9e60 # Parent b6fd2f4414620d4ef40217c940126842b4cfce03 updated syntax to use 'ML_file' rather than 'uses'; diff -r b6fd2f441462 -r a1a45fdc53a3 src/HOL/TPTP/lib/Tools/tptp_graph --- a/src/HOL/TPTP/lib/Tools/tptp_graph Tue Sep 03 21:46:41 2013 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_graph Tue Sep 03 21:46:41 2013 +0100 @@ -115,8 +115,8 @@ { LOADER="tptp_graph_$RANDOM" echo "theory $LOADER imports \"$TPTP_HOME/TPTP_Parser\" \ - uses \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \ - begin ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \ +begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \ +ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \ > $WORKDIR/$LOADER.thy "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\"; exit 0;" Pure }