diff -r 0028bd06a19c -r e7265e70fd7c src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/MicroJava/BV/Err.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -257,7 +257,7 @@
     [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |] 
     ==> x <=_r z \<and> y <=_r z"
     by (rule plus_le_conv [THEN iffD1])
-  case antecedent
+  case rule_context
   thus ?thesis
   apply (rule_tac iffI)
    apply clarify