diff -r dfae7eb2830c -r ec70653a02bf src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Fri Oct 17 11:04:36 2003 +0200
+++ b/src/Pure/meta_simplifier.ML	Tue Oct 21 11:09:23 2003 +0200
@@ -40,6 +40,9 @@
   val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
   val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
   val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
+  val get_mk_rews       : meta_simpset -> thm -> thm list
+  val get_mk_sym        : meta_simpset -> thm -> thm option
+  val get_mk_eq_True    : meta_simpset -> thm -> thm option
   val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
   val beta_eta_conversion: cterm -> thm
   val rewrite_cterm: bool * bool * bool ->
@@ -518,6 +521,10 @@
             {mk= #mk mk_rews, mk_sym= #mk_sym mk_rews, mk_eq_True= mk_eq_True},
             termless,depth);
 
+fun get_mk_rews    (Mss {mk_rews,...}) = #mk         mk_rews
+fun get_mk_sym     (Mss {mk_rews,...}) = #mk_sym     mk_rews
+fun get_mk_eq_True (Mss {mk_rews,...}) = #mk_eq_True mk_rews
+
 (* termless *)
 
 fun set_termless