diff -r a53f5db5acbb -r 73b8b42a36b6 src/HOL/HoareParallel/Mul_Gar_Coll.thy
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -383,8 +383,7 @@
 apply force
 --{* 1 subgoal left *}
 apply clarify
-apply(drule le_imp_less_or_eq)
-apply(disjE_tac)
+apply(drule Nat.le_imp_less_or_eq)
 apply (simp_all add:Blacks_def)
 done