diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/Nat.ML
--- a/src/ZF/Nat.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/Nat.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -36,7 +36,8 @@
 val nat_1I = result();
 
 goal Nat.thy "bool <= nat";
-by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1 ORELSE etac boolE 1));
+by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1
+	    ORELSE eresolve_tac [boolE,ssubst] 1));
 val bool_subset_nat = result();
 
 val bool_into_nat = bool_subset_nat RS subsetD;