--- a/src/HOLCF/ex/Dnat.thy	Sat Mar 13 19:06:18 2010 -0800
+++ b/src/HOLCF/ex/Dnat.thy	Sat Mar 13 20:15:25 2010 -0800
@@ -52,7 +52,7 @@
 
 lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y"
   apply (rule allI)
-  apply (induct_tac x rule: dnat.ind)
+  apply (induct_tac x)
     apply fast
    apply (rule allI)
    apply (case_tac y)