diff -r fbd346f5af86 -r 30950dadd09f thys/turing_hoare.thy
--- a/thys/turing_hoare.thy	Sat Jan 19 21:03:55 2013 +0000
+++ b/thys/turing_hoare.thy	Sun Jan 20 05:04:19 2013 +0000
@@ -2,6 +2,12 @@
 imports turing_basic
 begin
 
+declare step.simps[simp del]
+declare steps.simps[simp del]
+declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]
+declare tm_wf.simps[simp del]
+
+
 type_synonym assert = "tape \<Rightarrow> bool"
 
 definition 
@@ -66,7 +72,7 @@
   then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
     by(case_tac "steps0 (1, l, r) A n1") (auto)
   then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')"
-    using A_wf by(rule_tac t_merge_pre_halt_same) (auto)
+    using A_wf by(rule_tac tm_comp_pre_halt_same) (auto)
   moreover
   from c aimpb have "P2 holds_for (0, l', r')"
     by (rule holds_for_imp)
@@ -100,7 +106,7 @@
   fixes A B :: tprog0 
   assumes aimpb: "Q1 \<mapsto> P2"
   and A_wf : "tm_wf (A, 0)"
-  and B_wf : "tm_wf (B, 0)"
+  and B_wf : "tm_wf (B, 0)"  (* probably not needed *)
   and A_halt : "{P1} A {Q1}"
   and B_uhalt : "{P2} B"
   shows "{P1} (A |+| B)"
@@ -113,7 +119,7 @@
     by(case_tac "steps0 (1, l, r) A n1", auto)
   then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')"
     using A_wf
-    by(rule_tac t_merge_pre_halt_same, auto)
+    by(rule_tac tm_comp_pre_halt_same, auto)
   from c aimpb have "P2 holds_for (0, l', r')"
     by(rule holds_for_imp)
   from this have "P2 (l', r')" by auto