no more simp_legacy_precond
authornipkow
Mon May 04 16:01:36 2015 +0200 (2015-05-04)
changeset 60171b3be7677461e
parent 60170 031ec3d34d31
child 60172 423273355b55
no more simp_legacy_precond
NEWS
src/HOL/Tools/simpdata.ML
     1.1 --- a/NEWS	Mon May 04 10:22:13 2015 +0200
     1.2 +++ b/NEWS	Mon May 04 16:01:36 2015 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
    1.10  
    1.11  
    1.12  New in Isabelle2015 (May 2015)
     2.1 --- a/src/HOL/Tools/simpdata.ML	Mon May 04 10:22:13 2015 +0200
     2.2 +++ b/src/HOL/Tools/simpdata.ML	Mon May 04 16:01:36 2015 +0200
     2.3 @@ -115,13 +115,8 @@
     2.4  fun mksimps pairs ctxt =
     2.5    map_filter (try mk_eq) o mk_atomize ctxt pairs o Drule.gen_all (Variable.maxidx_of ctxt);
     2.6  
     2.7 -val simp_legacy_precond =
     2.8 -  Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false)
     2.9 -
    2.10  fun unsafe_solver_tac ctxt =
    2.11    let
    2.12 -    val intros =
    2.13 -      if Config.get ctxt simp_legacy_precond then [] else [@{thm conjI}]
    2.14      val sol_thms =
    2.15        reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
    2.16      fun sol_tac i =
    2.17 @@ -129,7 +124,8 @@
    2.18         [resolve_tac ctxt sol_thms i,
    2.19          assume_tac ctxt i,
    2.20          eresolve_tac ctxt @{thms FalseE} i] ORELSE
    2.21 -      (match_tac ctxt intros THEN_ALL_NEW sol_tac) i
    2.22 +          (match_tac ctxt [@{thm conjI}]
    2.23 +      THEN_ALL_NEW sol_tac) i
    2.24    in
    2.25      (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac
    2.26    end;