diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOLCF/ex/Dnat.thy
--- a/src/HOLCF/ex/Dnat.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOLCF/ex/Dnat.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -10,7 +10,7 @@
 domain dnat = dzero | dsucc (dpred :: dnat)
 
 definition
-  iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
+  iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" where
   "iterator = fix $ (LAM h n f x.
     case n of dzero => x
       | dsucc $ m => f $ (h $ m $ f $ x))"