diff -r fd242f857508 -r 0bec857c9871 doc-src/TutorialI/Advanced/Partial.thy
--- a/doc-src/TutorialI/Advanced/Partial.thy	Fri Sep 28 20:08:05 2001 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Fri Sep 28 20:08:28 2001 +0200
@@ -64,7 +64,7 @@
 consts divi :: "nat \<times> nat \<Rightarrow> nat"
 recdef (permissive) divi "measure(\<lambda>(m,n). m)"
   "divi(m,n) = (if n = 0 then arbitrary else
-                if m < n then 0 else divi(m-n,n)+1)"  (* FIXME permissive!? *)
+                if m < n then 0 else divi(m-n,n)+1)"  (* FIXME hide permissive!? *)
 
 text{*\noindent Of course we could also have defined
 @{term"divi(m,0)"} to be some specific number, for example 0. The