src/HOL/Real/PNat.ML

--- a/src/HOL/Real/PNat.ML	Wed Oct 11 00:03:22 2000 +0200
+++ b/src/HOL/Real/PNat.ML	Wed Oct 11 09:09:06 2000 +0200
@@ -10,7 +10,7 @@
 by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
 qed "pnat_fun_mono";
 
-bind_thm ("pnat_unfold", pnat_fun_mono RS (pnat_def RS def_lfp_Tarski));
+bind_thm ("pnat_unfold", pnat_fun_mono RS (pnat_def RS def_lfp_unfold));
 
 Goal "1 : pnat";
 by (stac pnat_unfold 1);