# HG changeset patch
# User blanchet
# Date 1385037822 -3600
# Node ID c999e2533487e5cd37e86629774f6354add44e64
# Parent  8b403a7a8c44755220bb1679884bca4a1e200c57
renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy

diff -r 8b403a7a8c44 -r c999e2533487 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Thu Nov 21 12:29:29 2013 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Thu Nov 21 13:43:42 2013 +0100
@@ -309,11 +309,11 @@
     val (format, type_enc, lam_trans) =
       (case format_str of
         "FOF" => (FOF, "mono_guards??", liftingN)
-      | "TFF0" => (TFF Monomorphic, "mono_native", liftingN)
-      | "THF0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
+      | "TF0" => (TFF Monomorphic, "mono_native", liftingN)
+      | "TH0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
       | "DFG" => (DFG Monomorphic, "mono_native", liftingN)
       | _ => error ("Unknown format " ^ quote format_str ^
-        " (expected \"FOF\", \"TFF0\", \"THF0\", or \"DFG\")"))
+        " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
     val uncurried_aliases = false
     val readable_names = true
     val presimp = true
diff -r 8b403a7a8c44 -r c999e2533487 src/HOL/TPTP/lib/Tools/tptp_translate
--- a/src/HOL/TPTP/lib/Tools/tptp_translate	Thu Nov 21 12:29:29 2013 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Thu Nov 21 13:43:42 2013 +0100
@@ -11,7 +11,7 @@
   echo
   echo "Usage: isabelle $PRG FORMAT FILE"
   echo
-  echo "  Translates TPTP input file to the specified format (\"FOF\", \"TFF0\", \"THF0\", or \"DFG\")."
+  echo "  Translates TPTP input file to the specified format (\"FOF\", \"TF0\", \"TH0\", or \"DFG\")."
   echo "  Emits the result to standard output."
   echo
   exit 1