src/HOL/Real/PNat.ML

--- a/src/HOL/Real/PNat.ML	Wed Jan 23 17:01:53 2002 +0100
+++ b/src/HOL/Real/PNat.ML	Wed Jan 23 17:13:54 2002 +0100
@@ -261,7 +261,7 @@
 Goalw [pnat_less_def] 
      "x < (y::pnat) ==> Rep_pnat y ~= Suc 0";
 by (auto_tac (claset(),simpset() 
-    addsimps [Rep_pnat_not_less_one] delsimps [less_one]));
+    addsimps [Rep_pnat_not_less_one] delsimps [less_Suc0]));
 qed "Rep_pnat_gt_implies_not0";
 
 Goalw [pnat_less_def]