# HG changeset patch
# User paulson
# Date 971345931 -7200
# Node ID 7b6f9d34f737b9032af89cf8675009af4ee27d4e
# Parent  2b255b772585851f58b216e3f9e723dbe5137051
delrules [r_into_rtrancl] required because the new I-rule made a step slow.
There must be others somehwere...

diff -r 2b255b772585 -r 7b6f9d34f737 src/HOL/BCV/JVM.ML
--- a/src/HOL/BCV/JVM.ML	Thu Oct 12 12:16:58 2000 +0200
+++ b/src/HOL/BCV/JVM.ML	Thu Oct 12 12:18:51 2000 +0200
@@ -187,10 +187,11 @@
 by (Asm_simp_tac 1);
 
 by (rtac conjI 1);
-by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1);
+by (force_tac (claset(), simpset() addsplits [list.split]) 1);
 
 by (rtac conjI 1);
-by (fast_tac (claset() addDs [rtrancl_trans]
+by (fast_tac (claset() delrules [r_into_rtrancl]
+		       addDs [rtrancl_trans]
        addss (simpset() addsplits [list.split])) 1);
 
 by (rtac conjI 1);