--- 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