diff -r f20cc66b2c74 -r 1b70db55c811 src/HOL/Mirabelle/doc/options.txt
--- a/src/HOL/Mirabelle/doc/options.txt	Sat Sep 05 11:45:57 2009 +0200
+++ b/src/HOL/Mirabelle/doc/options.txt	Sat Sep 05 15:46:52 2009 +0200
@@ -2,6 +2,5 @@
 
   * prover=NAME: name of the external prover to call
   * keep=PATH: path where to keep temporary files created by sledgehammer 
-  * metis=X: apply metis with the theorems found by sledgehammer (X may be any
-      non-empty string)
-  * full_types=X: turn on full-typed encoding (X may be any non-empty string)
+  * metis: apply metis with the theorems found by sledgehammer
+  * full_types: turn on full-typed encoding