--- a/src/Pure/Isar/isar_cmd.ML Wed Dec 05 03:15:32 2001 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Wed Dec 05 03:15:50 2001 +0100
@@ -49,6 +49,7 @@
val print_locales: Toplevel.transition -> Toplevel.transition
val print_locale: Locale.expr -> Toplevel.transition -> Toplevel.transition
val print_attributes: Toplevel.transition -> Toplevel.transition
+ val print_rules: Toplevel.transition -> Toplevel.transition
val print_induct_rules: Toplevel.transition -> Toplevel.transition
val print_trans_rules: Toplevel.transition -> Toplevel.transition
val print_methods: Toplevel.transition -> Toplevel.transition
@@ -198,6 +199,10 @@
val print_attributes = Toplevel.unknown_theory o
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
+val print_rules = Toplevel.unknown_context o
+ Toplevel.keep (Toplevel.node_case ContextRules.print_global_rules
+ (ContextRules.print_local_rules o Proof.context_of));
+
val print_induct_rules = Toplevel.unknown_context o
Toplevel.keep (Toplevel.node_case InductAttrib.print_global_rules
(InductAttrib.print_local_rules o Proof.context_of));