src/HOL/TPTP/lib/Tools/tptp_translate

--- a/src/HOL/TPTP/lib/Tools/tptp_translate	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Mon Jan 23 17:40:32 2012 +0100
@@ -9,21 +9,20 @@
 
 function usage() {
   echo
-  echo "Usage: isabelle $PRG FORMAT FILE"
+  echo "Usage: isabelle $PRG FORMAT IN_FILE OUT_FILE"
   echo
-  echo "  Translates TPTP file to specified TPTP format (\"CNF\", \"FOF\", \"TFF0\", \"TFF1\", or \"THF0\")."
+  echo "  Translates TPTP input file to specified TPTP format (\"CNF\", \"FOF\", \"TFF0\", \"TFF1\", or \"THF0\")."
   echo
   exit 1
 }
 
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+[ "$#" -ne 3 -o "$1" = "-?" ] && usage
 
 SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
 
-for FILE in "$@"
-do
-  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.translate_tptp_file \"$FILE\" *} end;" \
-    > /tmp/$SCRATCH.thy
-  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
-done
+args=("$@")
+
+echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.translate_tptp_file \"${args[0]}\" \"${args[1]}\" \"${args[2]}\" *} end;" \
+  > /tmp/$SCRATCH.thy
+"$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"