updated syntax to use 'ML_file' rather than 'uses';
authorsultana
Tue, 03 Sep 2013 21:46:41 +0100
changeset 53392 a1a45fdc53a3
parent 53391 b6fd2f441462
child 53393 5278312037f8
updated syntax to use 'ML_file' rather than 'uses';
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
 }