--- 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 =