diff -r 11bfb7e7cc86 -r b13515940b53 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Oct 11 18:02:14 2010 +0700
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Oct 11 18:03:18 2010 +0700
@@ -9,6 +9,7 @@
 
 signature METIS_TACTICS =
 sig
+  val trace : bool Config.T
   val type_lits : bool Config.T
   val new_skolemizer : bool Config.T
   val metis_tac : Proof.context -> thm list -> int -> tactic