src/HOL/Real/PNat.ML

--- a/src/HOL/Real/PNat.ML	Mon Oct 23 11:15:52 2000 +0200
+++ b/src/HOL/Real/PNat.ML	Mon Oct 23 15:20:15 2000 +0200
@@ -126,9 +126,7 @@
 (** alternative definition for pnat **)
 (** order isomorphism **)
 Goal "pnat = {x::nat. 0 < x}";
-by (rtac set_ext 1);
-by (simp_tac (simpset() addsimps 
-    [mem_pnat_gt_0_iff]) 1);
+by (auto_tac (claset(), simpset() addsimps [mem_pnat_gt_0_iff]));  
 qed "Collect_pnat_gt_0";
 
 (*** Distinctness of constructors ***)