diff -r 142f1eb707b4 -r befa4e9f7c90 Nat.ML
--- a/Nat.ML	Thu Sep 16 14:29:14 1993 +0200
+++ b/Nat.ML	Wed Sep 22 15:43:05 1993 +0200
@@ -351,6 +351,15 @@
 
 val nat_ss = pair_ss  addsimps  nat_simps;
 
+(*Prevents simplification of f and g: much faster*)
+val nat_case_weak_cong = prove_goal Nat.thy
+  "m=n ==> nat_case(m,a,f) = nat_case(n,a,f)"
+  (fn [prem] => [rtac (prem RS arg_cong) 1]);
+
+val nat_rec_weak_cong = prove_goal Nat.thy
+  "m=n ==> nat_rec(m,a,f) = nat_rec(n,a,f)"
+  (fn [prem] => [rtac (prem RS arg_cong) 1]);
+
 val prems = goalw Nat.thy [le_def] "~(n<m) ==> m<=n::nat";
 by (resolve_tac prems 1);
 val leI = result();