--- a/thys/Abacus.thy	Tue Sep 03 15:02:52 2013 +0100
+++ b/thys/Abacus.thy	Sat Nov 23 13:23:53 2013 +0000
@@ -546,9 +546,11 @@
 lemma compile_mod2: "length (concat (take n (tms_of ap))) mod 2 = 0"
 apply(induct n, auto)
 apply(case_tac "n < length (tms_of ap)", simp add: take_Suc_conv_app_nth, auto)
-apply(subgoal_tac "length (tms_of ap ! n) mod 2 = 0")
+(*apply(subgoal_tac "length (tms_of ap ! n) mod 2 = 0")
 apply arith
 by auto
+*)
+done
 
 lemma tpa_states:
   "\<lbrakk>tp = concat (take as (tms_of ap));