diff -r bea94f1e6771 -r dae7501b26ac prio/PrioG.thy
--- a/prio/PrioG.thy	Fri Apr 20 11:45:06 2012 +0000
+++ b/prio/PrioG.thy	Fri Apr 20 14:15:36 2012 +0000
@@ -2776,6 +2776,8 @@
 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
   where "detached s th \<equiv> (Th th \<notin> Field (depend s))"
 
+thm Field_def
+
 lemma detached_intro:
   fixes s th
   assumes vt: "vt s"
@@ -2803,12 +2805,14 @@
       have "holdents s th = {}"
         by (simp add:cntCS_def)
       thus ?thesis
-        by (auto simp:holdents_def, case_tac x, 
-          auto simp:holdents_def s_depend_def)
+        apply(auto simp:holdents_def)
+        apply(case_tac a)
+        apply(auto simp:holdents_def s_depend_def)
+        done
     qed
     ultimately show ?thesis
       apply (auto simp:detached_def Field_def Domain_def readys_def)
-      apply (case_tac y, auto simp:s_depend_def)
+      apply (case_tac b, auto simp:s_depend_def)
       by (erule_tac x = "nat" in allE, simp add: eq_waiting)
   qed
 qed