tuned;

--- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Feb 09 16:23:40 2001 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Feb 09 20:34:42 2001 +0100
@@ -189,8 +189,6 @@
 apply(erule (1) rtrancl_trans)
 done
 
-ML {* InductAttrib.print_global_rules(the_context()) *}
-ML {* set show_tags *}
 
 (*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
 proof -