--- a/Correctness.thy	Wed Jan 13 15:22:14 2016 +0000
+++ b/Correctness.thy	Wed Jan 13 23:39:59 2016 +0800
@@ -124,13 +124,16 @@
   qed
 qed
 
-locale red_extend_highest_gen = extend_highest_gen +
+(* locale red_extend_highest_gen = extend_highest_gen +
    fixes i::nat
+*)
 
+(*
 sublocale red_extend_highest_gen <   red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"
   apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
   apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
   by (unfold highest_gen_def, auto dest:step_back_vt_app)
+*)
 
 context extend_highest_gen
 begin
@@ -790,5 +793,6 @@
   thus ?thesis using th_blockedE by auto
 qed
 
+
 end
 end