--- a/prio/PrioG.thy	Thu Feb 09 13:05:51 2012 +0000
+++ b/prio/PrioG.thy	Thu Feb 09 15:00:19 2012 +0000
@@ -789,8 +789,8 @@
   "vt step (P th cs#s) \<Longrightarrow>
   depend (P th cs # s) =  (if (wq s cs = []) then depend s \<union> {(Cs cs, Th th)}
                                              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(simp only: s_depend_def wq_def)
+  apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def)
   apply(case_tac "csa = cs", auto)
   apply(fold wq_def)
   apply(drule_tac step_back_step)