--- a/thys/turing_hoare.thy	Mon Jan 28 02:38:57 2013 +0000
+++ b/thys/turing_hoare.thy	Tue Jan 29 12:37:06 2013 +0000
@@ -36,7 +36,7 @@
 
 (* not halting case *)
 definition
-  Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50)
+  Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" 50)
 where
   "{P} p \<up> \<equiv> \<forall>tp. P tp \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, tp) p n)))"