diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Recdef/simplification.thy
--- a/doc-src/TutorialI/Recdef/simplification.thy	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Wed Dec 12 09:04:20 2001 +0100
@@ -19,7 +19,7 @@
 text{*\noindent
 According to the measure function, the second argument should decrease with
 each recursive call. The resulting termination condition
-@{term[display]"n ~= 0 ==> m mod n < n"}
+@{term[display]"n ~= (0::nat) ==> m mod n < n"}
 is proved automatically because it is already present as a lemma in
 HOL\@.  Thus the recursion equation becomes a simplification
 rule. Of course the equation is nonterminating if we are allowed to unfold
@@ -58,7 +58,7 @@
 
 text{*\noindent
 The order of equations is important: it hides the side condition
-@{prop"n ~= 0"}.  Unfortunately, in general the case distinction
+@{prop"n ~= (0::nat)"}.  Unfortunately, in general the case distinction
 may not be expressible by pattern matching.
 
 A simple alternative is to replace @{text if} by @{text case},