# HG changeset patch # User wenzelm # Date 1236375147 -3600 # Node ID 3d03190d28642aa6e49aa8d92d4641e558a96a90 # Parent 159bab53b40d9dd6ac892e0ea5345e8b8ef894a5 replaced archaic use of rep_ss by Simplifier.mksimps; diff -r 159bab53b40d -r 3d03190d2864 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Fri Mar 06 21:49:58 2009 +0100 +++ b/src/Pure/Tools/find_theorems.ML Fri Mar 06 22:32:27 2009 +0100 @@ -168,8 +168,7 @@ fun etacn thm i = Seq.take (! tac_limit) o etac thm i; fun try_thm thm = if Thm.no_prems thm then rtac thm 1 goal - else (etacn thm THEN_ALL_NEW - (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; + else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; in fn (_, thm) => if (is_some o Seq.pull o try_thm) thm @@ -181,11 +180,10 @@ fun filter_simp ctxt t (_, thm) = let - val (_, {mk_rews = {mk, ...}, ...}) = - Simplifier.rep_ss (Simplifier.local_simpset_of ctxt); + val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt); val extract_simp = - (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl); - val ss = is_matching_thm extract_simp ctxt false t thm + (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); + val ss = is_matching_thm extract_simp ctxt false t thm; in if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE end; diff -r 159bab53b40d -r 3d03190d2864 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Fri Mar 06 21:49:58 2009 +0100 +++ b/src/Pure/meta_simplifier.ML Fri Mar 06 22:32:27 2009 +0100 @@ -59,6 +59,7 @@ val delcongs: simpset * thm list -> simpset val addsimprocs: simpset * simproc list -> simpset val delsimprocs: simpset * simproc list -> simpset + val mksimps: simpset -> thm -> thm list val setmksimps: simpset * (thm -> thm list) -> simpset val setmkcong: simpset * (thm -> thm) -> simpset val setmksym: simpset * (thm -> thm option) -> simpset @@ -547,6 +548,7 @@ fun add_simp thm ss = ss addsimps [thm]; fun del_simp thm ss = ss delsimps [thm]; + (* congs *) fun cong_name (Const (a, _)) = SOME a @@ -694,6 +696,8 @@ in +val mksimps = #mk o #mk_rews o #2 o rep_ss; + fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) => (mk, mk_cong, mk_sym, mk_eq_True, reorient)); diff -r 159bab53b40d -r 3d03190d2864 src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Fri Mar 06 21:49:58 2009 +0100 +++ b/src/Tools/eqsubst.ML Fri Mar 06 22:32:27 2009 +0100 @@ -128,8 +128,7 @@ (* changes object "=" to meta "==" which prepares a given rewrite rule *) fun prep_meta_eq ctxt = - let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt) - in mk #> map Drule.zero_var_indexes end; + Simplifier.mksimps (Simplifier.local_simpset_of ctxt) #> map Drule.zero_var_indexes; (* a type abriviation for match information *)