--- a/Nat.ML Thu Nov 24 20:31:09 1994 +0100
+++ b/Nat.ML Fri Nov 25 09:12:16 1994 +0100
@@ -354,11 +354,11 @@
val nat_ss0 = sum_ss addsimps nat_simps;
(*Prevents simplification of f and g: much faster*)
-val nat_case_weak_cong = prove_goal Nat.thy
+qed_goal "nat_case_weak_cong" Nat.thy
"m=n ==> nat_case(a,f,m) = nat_case(a,f,n)"
(fn [prem] => [rtac (prem RS arg_cong) 1]);
-val nat_rec_weak_cong = prove_goal Nat.thy
+qed_goal "nat_rec_weak_cong" Nat.thy
"m=n ==> nat_rec(m,a,f) = nat_rec(n,a,f)"
(fn [prem] => [rtac (prem RS arg_cong) 1]);