replaced archaic use of rep_ss by Simplifier.mksimps;
authorwenzelm
Fri Mar 06 22:32:27 2009 +0100 (2009-03-06)
changeset 303183d03190d2864
parent 30317 159bab53b40d
child 30319 a549dc15c037
replaced archaic use of rep_ss by Simplifier.mksimps;
src/Pure/Tools/find_theorems.ML
src/Pure/meta_simplifier.ML
src/Tools/eqsubst.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Mar 06 21:49:58 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Mar 06 22:32:27 2009 +0100
     1.3 @@ -168,8 +168,7 @@
     1.4      fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
     1.5      fun try_thm thm =
     1.6        if Thm.no_prems thm then rtac thm 1 goal
     1.7 -      else (etacn thm THEN_ALL_NEW
     1.8 -             (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
     1.9 +      else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
    1.10    in
    1.11      fn (_, thm) =>
    1.12        if (is_some o Seq.pull o try_thm) thm
    1.13 @@ -181,11 +180,10 @@
    1.14  
    1.15  fun filter_simp ctxt t (_, thm) =
    1.16    let
    1.17 -    val (_, {mk_rews = {mk, ...}, ...}) =
    1.18 -      Simplifier.rep_ss (Simplifier.local_simpset_of ctxt);
    1.19 +    val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt);
    1.20      val extract_simp =
    1.21 -      (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
    1.22 -    val ss = is_matching_thm extract_simp ctxt false t thm
    1.23 +      (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
    1.24 +    val ss = is_matching_thm extract_simp ctxt false t thm;
    1.25    in
    1.26      if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
    1.27    end;
     2.1 --- a/src/Pure/meta_simplifier.ML	Fri Mar 06 21:49:58 2009 +0100
     2.2 +++ b/src/Pure/meta_simplifier.ML	Fri Mar 06 22:32:27 2009 +0100
     2.3 @@ -59,6 +59,7 @@
     2.4    val delcongs: simpset * thm list -> simpset
     2.5    val addsimprocs: simpset * simproc list -> simpset
     2.6    val delsimprocs: simpset * simproc list -> simpset
     2.7 +  val mksimps: simpset -> thm -> thm list
     2.8    val setmksimps: simpset * (thm -> thm list) -> simpset
     2.9    val setmkcong: simpset * (thm -> thm) -> simpset
    2.10    val setmksym: simpset * (thm -> thm option) -> simpset
    2.11 @@ -547,6 +548,7 @@
    2.12  fun add_simp thm ss = ss addsimps [thm];
    2.13  fun del_simp thm ss = ss delsimps [thm];
    2.14  
    2.15 +
    2.16  (* congs *)
    2.17  
    2.18  fun cong_name (Const (a, _)) = SOME a
    2.19 @@ -694,6 +696,8 @@
    2.20  
    2.21  in
    2.22  
    2.23 +val mksimps = #mk o #mk_rews o #2 o rep_ss;
    2.24 +
    2.25  fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
    2.26    (mk, mk_cong, mk_sym, mk_eq_True, reorient));
    2.27  
     3.1 --- a/src/Tools/eqsubst.ML	Fri Mar 06 21:49:58 2009 +0100
     3.2 +++ b/src/Tools/eqsubst.ML	Fri Mar 06 22:32:27 2009 +0100
     3.3 @@ -128,8 +128,7 @@
     3.4  
     3.5  (* changes object "=" to meta "==" which prepares a given rewrite rule *)
     3.6  fun prep_meta_eq ctxt =
     3.7 -  let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
     3.8 -  in mk #> map Drule.zero_var_indexes end;
     3.9 +  Simplifier.mksimps (Simplifier.local_simpset_of ctxt) #> map Drule.zero_var_indexes;
    3.10  
    3.11  
    3.12    (* a type abriviation for match information *)