--- a/src/HOL/UNITY/Comp/AllocBase.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Thu Jul 15 13:11:34 2004 +0200
@@ -87,8 +87,8 @@
lemma bag_of_sublist_Un_Int:
"bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =
bag_of (sublist l A) + bag_of (sublist l B)"
-apply (subgoal_tac "A Int B Int {..length l (} =
- (A Int {..length l (}) Int (B Int {..length l (}) ")
+apply (subgoal_tac "A Int B Int {..<length l} =
+ (A Int {..<length l}) Int (B Int {..<length l}) ")
apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast)
done