diff -r 13c5469b4bb3 -r d2758965362e doc-src/TutorialI/Inductive/Advanced.thy
--- a/doc-src/TutorialI/Inductive/Advanced.thy	Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Advanced.thy	Mon Nov 12 10:56:38 2001 +0100
@@ -76,6 +76,7 @@
 by (blast intro!: mono_Int monoI gterms_mono)
 
 
+text{*the following declaration isn't actually used*}
 consts integer_arity :: "integer_op \<Rightarrow> nat"
 primrec
 "integer_arity (Number n)        = 0"