# HG changeset patch
# User nipkow
# Date 1430748096 -7200
# Node ID b3be7677461ecc78cf33104a986c58023a2c75f2
# Parent  031ec3d34d3192ca9decf95392caff0b119786dc
no more simp_legacy_precond

diff -r 031ec3d34d31 -r b3be7677461e NEWS
--- a/NEWS	Mon May 04 10:22:13 2015 +0200
+++ b/NEWS	Mon May 04 16:01:36 2015 +0200
@@ -6,6 +6,9 @@
 New in this Isabelle version
 ----------------------------
 
+*** HOL ***
+
+* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
 
 
 New in Isabelle2015 (May 2015)
diff -r 031ec3d34d31 -r b3be7677461e src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Mon May 04 10:22:13 2015 +0200
+++ b/src/HOL/Tools/simpdata.ML	Mon May 04 16:01:36 2015 +0200
@@ -115,13 +115,8 @@
 fun mksimps pairs ctxt =
   map_filter (try mk_eq) o mk_atomize ctxt pairs o Drule.gen_all (Variable.maxidx_of ctxt);
 
-val simp_legacy_precond =
-  Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false)
-
 fun unsafe_solver_tac ctxt =
   let
-    val intros =
-      if Config.get ctxt simp_legacy_precond then [] else [@{thm conjI}]
     val sol_thms =
       reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
     fun sol_tac i =
@@ -129,7 +124,8 @@
        [resolve_tac ctxt sol_thms i,
         assume_tac ctxt i,
         eresolve_tac ctxt @{thms FalseE} i] ORELSE
-      (match_tac ctxt intros THEN_ALL_NEW sol_tac) i
+          (match_tac ctxt [@{thm conjI}]
+      THEN_ALL_NEW sol_tac) i
   in
     (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac
   end;