diff -r 28dae2b40c6f -r 08d34921b7dd src/HOL/Mirabelle/lib/Tools/mirabelle
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Tue Dec 08 18:47:25 2009 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Tue Dec 08 23:05:23 2009 +0100
@@ -46,6 +46,8 @@
   echo "    * minimize_timeout=TIME: timeout for each minimization step (seconds of"
   echo "      process time)"
   echo "    * metis: apply metis to the theorems found by sledgehammer"
+  echo "    * metis_ft: apply metis with fully-typed encoding to the theorems found"
+  echo "      by sledgehammer"
   echo
   echo "  FILES is a list of theory files, where each file is either NAME.thy"
   echo "  or NAME.thy[START:END] and START and END are numbers indicating the"