# HG changeset patch
# User wenzelm
# Date 1003857287 -7200
# Node ID 77c63f8e9d9aedf6fc06a084fa581dbbb286d632
# Parent  3a4b3c311a978e1ee82a15fdc854e79f42f4f2f9
trace_rules: only non-empty;

diff -r 3a4b3c311a97 -r 77c63f8e9d9a src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Oct 23 19:14:31 2001 +0200
+++ b/src/Pure/Isar/method.ML	Tue Oct 23 19:14:47 2001 +0200
@@ -133,7 +133,7 @@
 val trace_rules = ref false;
 
 fun trace rules =
-  if not (! trace_rules) then ()
+  if not (! trace_rules) orelse null rules then ()
   else Pretty.writeln (Pretty.big_list "rules:" (map Display.pretty_thm rules));