--- a/prio/PrioG.thy	Wed Feb 08 16:35:49 2012 +0000
+++ b/prio/PrioG.thy	Thu Feb 09 13:05:51 2012 +0000
@@ -791,11 +791,12 @@
                                              else depend s \<union> {(Th th, Cs cs)})"
   apply(unfold s_depend_def wq_def)
   apply (auto split:list.splits prod.splits simp:Let_def cs_waiting_def cs_holding_def)
-  apply(case_tac "c = cs", auto)
+  apply(case_tac "csa = cs", auto)
   apply(fold wq_def)
   apply(drule_tac step_back_step)
-  by (ind_cases " step s (P (hd (wq s cs)) cs)", 
-    auto simp:s_depend_def wq_def cs_holding_def)
+  apply(ind_cases " step s (P (hd (wq s cs)) cs)")
+  apply(auto simp:s_depend_def wq_def cs_holding_def)
+  done
 
 lemma simple_A:
   fixes A