# HG changeset patch
# User haftmann
# Date 1248265231 -7200
# Node ID b513db807fcad2c698212e7e36d0bda338278da7
# Parent  d2aea34845d42176187b9c36187d4326851ff29c
spurious proof failure

diff -r d2aea34845d4 -r b513db807fca src/HOL/HoareParallel/Mul_Gar_Coll.thy
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Wed Jul 22 08:05:33 2009 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Wed Jul 22 14:20:31 2009 +0200
@@ -1263,7 +1263,7 @@
  apply(simp add: Mul_Mutator_def mul_collector_defs mul_mutator_defs nth_append)
  apply force
 apply clarify
-apply(case_tac xa)
+apply(case_tac i)
  apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
 apply(simp add: Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append nth_map_upt)
 --{* Collector *}