# HG changeset patch
# User wenzelm
# Date 981747282 -3600
# Node ID 08690b7c0568cd1c28fe2b28587589e56d325866
# Parent  5a40937c6c4d064dbfc447d55670d5699e1eb4b0
tuned;

diff -r 5a40937c6c4d -r 08690b7c0568 src/HOL/MicroJava/J/TypeRel.thy
--- 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 -