diff -r 44428ea53dc1 -r c84278efa9d5 src/Doc/Tutorial/Misc/AdvancedInd.thy
--- a/src/Doc/Tutorial/Misc/AdvancedInd.thy	Wed Aug 29 12:07:45 2012 +0200
+++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy	Wed Aug 29 12:07:57 2012 +0200
@@ -132,8 +132,8 @@
 function:
 *};
 
-consts f :: "nat \<Rightarrow> nat";
-axioms f_ax: "f(f(n)) < f(Suc(n))";
+axiomatization f :: "nat \<Rightarrow> nat"
+  where f_ax: "f(f(n)) < f(Suc(n))"
 
 text{*
 \begin{warn}