# HG changeset patch
# User wenzelm
# Date 881241097 -3600
# Node ID 4d84cdb0df423178c8c3ec9d57ba9dac7c87d06d
# Parent  fbb275398eb7d475f730690b31d70ff6f5e55369
added print_simpset;

diff -r fbb275398eb7 -r 4d84cdb0df42 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Dec 04 13:50:43 1997 +0100
+++ b/src/Provers/simplifier.ML	Thu Dec 04 14:11:37 1997 +0100
@@ -26,6 +26,7 @@
            finish_tac: thm list -> int -> tactic,
     unsafe_finish_tac: thm list -> int -> tactic};
   val print_ss: simpset -> unit
+  val print_simpset: theory -> unit
   val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
   val setloop:      simpset *             (int -> tactic) -> simpset
   val addloop:      simpset *             (int -> tactic) -> simpset
@@ -246,6 +247,8 @@
 
 (* access simpset *)
 
+fun print_simpset thy = Display.print_data thy simpsetK;
+
 fun simpset_ref_of_sg sg =
   (case Sign.get_data sg simpsetK of
     SimpsetData r => r