diff -r 6c05c4632949 -r b9e1d53124f5 src/Doc/Tutorial/Misc/AdvancedInd.thy
--- a/src/Doc/Tutorial/Misc/AdvancedInd.thy	Sat May 28 17:35:12 2016 +0200
+++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy	Sat May 28 21:38:58 2016 +0200
@@ -133,7 +133,7 @@
 *}
 
 axiomatization f :: "nat \<Rightarrow> nat"
-  where f_ax: "f(f(n)) < f(Suc(n))"
+  where f_ax: "f(f(n)) < f(Suc(n))" for n :: nat
 
 text{*
 \begin{warn}