diff -r c80a08ff2a85 -r 420e03a2d9cc Correctness.thy
--- 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: