--- a/Correctness.thy	Mon Mar 21 14:41:40 2016 +0000
+++ b/Correctness.thy	Mon Mar 21 15:06:52 2016 +0000
@@ -49,7 +49,7 @@
 
 -- {* @{term s} is a valid trace, so it will inherit all results derived for
       a valid trace: *}
-sublocale highest_gen < vat_s: valid_trace "s"
+sublocale highest_gen < vat_s?: valid_trace "s"
   by (unfold_locales, insert vt_s, simp)
 
 context highest_gen
@@ -98,7 +98,7 @@
   and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"
   and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"
 
-sublocale extend_highest_gen < vat_t: valid_trace "t@s"
+sublocale extend_highest_gen < vat_t?: valid_trace "t@s"
   by (unfold_locales, insert vt_t, simp)
 
 lemma step_back_vt_app: 

--- a/Implementation.thy	Mon Mar 21 14:41:40 2016 +0000
+++ b/Implementation.thy	Mon Mar 21 15:06:52 2016 +0000
@@ -29,7 +29,7 @@
     from tranclD[OF this]
     obtain z where "(Th th, z) \<in> RAG s" by auto
     with assms(1) have False
-         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
+         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_raw)
          by (fold wq_def, blast)
   } thus ?thesis by (unfold root_def, auto)
 qed
@@ -668,7 +668,7 @@
   have "Th th \<notin> Range (RAG s)"
   proof
     assume "Th th \<in> Range (RAG s)"
-    then obtain cs where "holding (wq s) th cs"
+    then obtain cs where "holding_raw (wq s) th cs"
       by (unfold Range_iff s_RAG_def, auto)
     with holdents_th_s[unfolded holdents_def]
     show False by (unfold holding_eq, auto)
@@ -676,7 +676,7 @@
   moreover have "Th th \<notin> Domain (RAG s)"
   proof
     assume "Th th \<in> Domain (RAG s)"
-    then obtain cs where "waiting (wq s) th cs"
+    then obtain cs where "waiting_raw (wq s) th cs"
       by (unfold Domain_iff s_RAG_def, auto)
     with th_ready_s show False by (unfold readys_def waiting_eq, auto)
   qed

--- a/Test.thy	Mon Mar 21 14:41:40 2016 +0000
+++ b/Test.thy	Mon Mar 21 15:06:52 2016 +0000
@@ -285,7 +285,7 @@
   shows "single_valuedP (waits2 s)"
 using assms
 unfolding single_valued_def
-by (metis Collect_splitD fst_eqD sndI waits2_unique)
+by (simp add: Product_Type.Collect_case_prodD waits2_unique)
 
 lemma single_valued_holds2:
   assumes "vt s"