diff -r 8ce9a432680b -r e6b13c7b9494 prio/CpsG.thy
--- a/prio/CpsG.thy	Mon Apr 23 08:01:37 2012 +0000
+++ b/prio/CpsG.thy	Mon Apr 30 15:32:34 2012 +0000
@@ -21,7 +21,7 @@
       assume eq_e: "e = Create thread prio"
         and not_in': "thread \<notin> threads s"
       have "holdents (e # s) th = holdents s th"
-        apply (unfold eq_e holdents_def)
+        apply (unfold eq_e holdents_test)
         by (simp add:depend_create_unchanged)
       moreover have "th \<notin> threads s" 
       proof -
@@ -37,13 +37,13 @@
         case True
         with nh eq_e
         show ?thesis 
-          by (auto simp:holdents_def depend_exit_unchanged)
+          by (auto simp:holdents_test depend_exit_unchanged)
       next
         case False
         with not_in and eq_e
         have "th \<notin> threads s" by simp
         from ih[OF this] False eq_e show ?thesis 
-          by (auto simp:holdents_def depend_exit_unchanged)
+          by (auto simp:holdents_test depend_exit_unchanged)
       qed
     next
       case (thread_P thread cs)
@@ -58,7 +58,7 @@
         ultimately show ?thesis by auto
       qed
       hence "holdents (e # s) th  = holdents s th "
-        apply (unfold cntCS_def holdents_def eq_e)
+        apply (unfold cntCS_def holdents_test eq_e)
         by (unfold step_depend_p[OF vtp], auto)
       moreover have "holdents s th = {}"
       proof(rule ih)
@@ -101,7 +101,7 @@
       qed
       moreover note neq_th eq_wq
       ultimately have "holdents (e # s) th  = holdents s th"
-        by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto)
+        by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto)
       moreover have "holdents s th = {}"
       proof(rule ih)
         from not_in eq_e show "th \<notin> threads s" by simp
@@ -115,13 +115,13 @@
       from not_in and eq_e have "th \<notin> threads s" by auto
       from ih [OF this] and eq_e
       show ?thesis 
-        apply (unfold eq_e cntCS_def holdents_def)
+        apply (unfold eq_e cntCS_def holdents_test)
         by (simp add:depend_set_unchanged)
     qed
     next
       case vt_nil
       show ?case
-      by (auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)
+      by (auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)
   qed
 qed
 
@@ -1919,7 +1919,7 @@
         from tranclE[OF this] obtain cs' where 
           "(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def)
         with hdn
-        have False by (auto simp:holdents_def)
+        have False by (auto simp:holdents_test)
       } thus ?thesis by auto
     qed
     thus ?thesis