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