diff -r 1ab41ea5b1c6 -r 631adf003bb0 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Mar 20 13:02:07 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Mar 20 13:53:09 2012 +0100
@@ -32,7 +32,7 @@
 val new_skolemizer =
   Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
 val advisory_simp =
-  Attrib.setup_config_bool @{binding metis_advisory_simp} (K false)
+  Attrib.setup_config_bool @{binding metis_advisory_simp} (K true)
 
 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
 fun have_common_thm ths1 ths2 =