src/HOL/Tools/Metis/metis_tactic.ML
changeset 47045 631adf003bb0
parent 47039 1b36a05a070d
child 47047 10bece4ac87e
--- 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 =