added dest_ss;
proper context fo pretty_ss;
tuned;

--- a/src/Pure/meta_simplifier.ML	Sun Mar 08 00:41:52 2009 +0100
+++ b/src/Pure/meta_simplifier.ML	Sun Mar 08 12:15:58 2009 +0100
@@ -24,7 +24,14 @@
   val mk_solver: string -> (thm list -> int -> tactic) -> solver
   val empty_ss: simpset
   val merge_ss: simpset * simpset -> simpset
-  val pretty_ss: simpset -> Pretty.T
+  val dest_ss: simpset ->
+   {simps: (string * thm) list,
+    procs: (string * cterm list) list,
+    congs: (string * thm) list,
+    weak_congs: string list,
+    loopers: string list,
+    unsafe_solvers: string list,
+    safe_solvers: string list}
   type simproc
   val eq_simproc: simproc * simproc -> bool
   val morph_simproc: morphism -> simproc -> simproc
@@ -325,35 +332,6 @@
 end;
 
 
-(* print simpsets *)
-
-fun pretty_ss ss =
-  let
-    val pretty_thms = map Display.pretty_thm;
-
-    fun pretty_cong (name, {thm, lhs}) =
-      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, Display.pretty_thm thm];
-    fun pretty_proc (name, lhss) =
-      Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
-
-    val Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...}) = ss;
-    val smps = map #thm (Net.entries rules);
-    val prcs = Net.entries procs |>
-      map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
-      |> partition_eq (eq_snd eq_procid)
-      |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps))
-      |> Library.sort_wrt fst;
-  in
-    [Pretty.big_list "simplification rules:" (pretty_thms smps),
-      Pretty.big_list "simplification procedures:" (map pretty_proc prcs),
-      Pretty.big_list "congruences:" (map pretty_cong (fst congs)),
-      Pretty.strs ("loopers:" :: map (quote o fst) loop_tacs),
-      Pretty.strs ("unsafe solvers:" :: map (quote o solver_name) (#1 solvers)),
-      Pretty.strs ("safe solvers:" :: map (quote o solver_name) (#2 solvers))]
-    |> Pretty.chunks
-  end;
-
-
 
 (** simpset operations **)
 
@@ -806,7 +784,7 @@
       val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
        {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
         loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
-  
+
       val rules' = Net.merge eq_rrule (rules1, rules2);
       val prems' = merge Thm.eq_thm_prop (prems1, prems2);
       val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
@@ -823,6 +801,22 @@
     end;
 
 
+(* dest_ss *)
+
+fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) =
+ {simps = Net.entries rules
+    |> map (fn {name, thm, ...} => (name, thm)),
+  procs = Net.entries procs
+    |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
+    |> partition_eq (eq_snd eq_procid)
+    |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
+  congs = map (fn (name, {thm, ...}) => (name, thm)) (#1 congs),
+  weak_congs = #2 congs,
+  loopers = map fst loop_tacs,
+  unsafe_solvers = map solver_name (#1 solvers),
+  safe_solvers = map solver_name (#2 solvers)};
+
+
 
 (** rewriting **)
 

--- a/src/Pure/simplifier.ML	Sun Mar 08 00:41:52 2009 +0100
+++ b/src/Pure/simplifier.ML	Sun Mar 08 12:15:58 2009 +0100
@@ -42,6 +42,7 @@
 signature SIMPLIFIER =
 sig
   include BASIC_SIMPLIFIER
+  val pretty_ss: Proof.context -> simpset -> Pretty.T
   val clear_ss: simpset -> simpset
   val debug_bounds: bool ref
   val inherit_context: simpset -> simpset -> simpset
@@ -86,6 +87,29 @@
 open MetaSimplifier;
 
 
+(** pretty printing **)
+
+fun pretty_ss ctxt ss =
+  let
+    val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
+    val pretty_thm = ProofContext.pretty_thm ctxt;
+    fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss);
+    fun pretty_cong (name, thm) =
+      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
+
+    val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
+  in
+    [Pretty.big_list "simplification rules:" (map (pretty_thm o #2) simps),
+      Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
+      Pretty.big_list "congruences:" (map pretty_cong congs),
+      Pretty.strs ("loopers:" :: map quote loopers),
+      Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
+      Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
+    |> Pretty.chunks
+  end;
+
+
+
 (** simpset data **)
 
 structure SimpsetData = GenericDataFun