diff -r da15d528fb19 -r f4f9946ad741 nat.ML
--- a/nat.ML	Thu Nov 25 10:04:02 1993 +0100
+++ b/nat.ML	Mon Nov 29 18:35:02 1993 +0100
@@ -349,7 +349,7 @@
 	     Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq, 
 	     nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
 
-val nat_ss = pair_ss  addsimps  nat_simps;
+val nat_ss = sum_ss  addsimps  nat_simps;
 
 (*Prevents simplification of f and g: much faster*)
 val nat_case_weak_cong = prove_goal Nat.thy