no more simp_legacy_precond

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

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