added trace_rules, trace;

--- a/src/Pure/Isar/method.ML	Fri Oct 12 12:08:57 2001 +0200
+++ b/src/Pure/Isar/method.ML	Fri Oct 12 12:09:21 2001 +0200
@@ -8,6 +8,7 @@
 
 signature BASIC_METHOD =
 sig
+  val trace_rules: bool ref
   val print_methods: theory -> unit
   val Method: bstring -> (Args.src -> Proof.context -> Proof.method) -> string -> unit
 end;
@@ -15,6 +16,7 @@
 signature METHOD =
 sig
   include BASIC_METHOD
+  val trace: thm list -> unit
   val print_global_rules: theory -> unit
   val print_local_rules: Proof.context -> unit
   val dest_global: theory attribute
@@ -123,6 +125,16 @@
 struct
 
 
+(** tracing *)
+
+val trace_rules = ref false;
+
+fun trace rules =
+  if not (! trace_rules) then ()
+  else Pretty.writeln (Pretty.big_list "rules:" (map Display.pretty_thm rules));
+
+
+
 (** global and local rule data **)
 
 local
@@ -323,7 +335,7 @@
     if not (null arg_rules) then arg_rules
     else if null facts then #1 (LocalRules.get ctxt)
     else op @ (LocalRules.get ctxt);
-  in tac rules facts end;
+  in trace rules; tac rules facts end;
 
 fun meth tac x = METHOD (HEADGOAL o tac x);
 fun meth' tac x y = METHOD (HEADGOAL o tac x y);