diff -r 12dd5d2e266b -r 978854c19b5e Nat.ML
--- 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]);