diff -r 1e45b5b6482a -r ca1fe315cb0a thys2/Turing2.thy
--- a/thys2/Turing2.thy	Fri May 24 15:43:10 2013 +0100
+++ b/thys2/Turing2.thy	Fri May 24 20:35:28 2013 +0100
@@ -58,11 +58,6 @@
   "steps cf p 0 = cf" |
   "steps cf p (Suc n) = steps (step cf p) p n"
 
-fun
-  is_final :: "config \<Rightarrow> bool"
-where
-  "is_final cf = (fst cf = 0)"
-
 
 (* well-formedness of Turing machine programs *)
 
@@ -114,7 +109,13 @@
 end
 
 definition 
-  "std_tape tp \<equiv> \<exists>k l (n::nat). tp = (Bk \<up> k, <n> @ Bk \<up> l)"
+  "std_tape tp \<equiv> \<exists>k (n::nat) l. snd tp = (Bk \<up> k, <n> @ Bk \<up> l)"
+
+fun
+  is_final :: "config \<Rightarrow> bool"
+where
+  "is_final cf = (fst cf = 0)"
+
 
 
 end