# HG changeset patch
# User wenzelm
# Date 1007518550 -3600
# Node ID 8896d7f494225142abc9561eb405c539dbaaa327
# Parent  5177845a34f5dbab02abdd2d5c5f11761f9fd428
added print_rules;

diff -r 5177845a34f5 -r 8896d7f49422 src/Pure/Isar/isar_cmd.ML
--- 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));