diff -r e6add51fd7ba -r 24d8c9e9dae4 src/HOL/Mirabelle/lib/Tools/mirabelle
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Sat Apr 14 23:52:17 2012 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Sat Apr 14 23:52:17 2012 +0100
@@ -15,6 +15,11 @@
   done
 }
 
+function print_sledgehammer_options() {
+  grep -e "^val .*K =" $MIRABELLE_HOME/Actions/mirabelle_sledgehammer.ML \
+  | perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/    $1$2/'
+}
+
 function usage() {
   [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None"
   timeout="$MIRABELLE_TIMEOUT"
@@ -36,18 +41,7 @@
   print_action_names
   echo
   echo "  Available OPTIONs for the ACTION sledgehammer:"
-  echo "    * prover=NAME: name of the external prover to call"
-  echo "    * prover_timeout=TIME: timeout for invoked ATP (seconds of process time)"
-  echo "    * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed"
-  echo "      time)"
-  echo "    * keep=PATH: path where to keep temporary files created by sledgehammer"
-  echo "    * full_types: enable fully-typed encoding"
-  echo "    * minimize: enable minimization of theorem set found by sledgehammer"
-  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"
+  print_sledgehammer_options
   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"