diff -r 5974111de158 -r f1ecb4a68a54 thys/Turing.thy
--- a/thys/Turing.thy	Thu Feb 21 05:33:57 2013 +0000
+++ b/thys/Turing.thy	Thu Feb 21 05:34:39 2013 +0000
@@ -205,16 +205,19 @@
   "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"
 
 fun 
-  adjust :: "instr list \<Rightarrow> instr list"
+  adjust :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"
 where
-  "adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"
+  "adjust p e = map (\<lambda> (a, s). (a, if s = 0 then e else s)) p"
+
+abbreviation
+  "adjust0 p \<equiv> adjust p (Suc (length p div 2))"
 
 lemma length_shift [simp]: 
   shows "length (shift p n) = length p"
 by simp
 
 lemma length_adjust [simp]: 
-  shows "length (adjust p) = length p"
+  shows "length (adjust p n) = length p"
 by (induct p) (auto)
 
 
@@ -222,7 +225,7 @@
 fun
   tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100)
 where
-  "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))"
+  "tm_comp p1 p2 = ((adjust0 p1) @ (shift p2 (length p1 div 2)))"
 
 lemma tm_comp_length:
   shows "length (A |+| B) = length A + length B"