diff -r 4d0545e93c0d -r c533bc92e882 Nat.ML
--- a/Nat.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/Nat.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -95,9 +95,9 @@
 by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
 qed "Suc_not_Zero";
 
-val Zero_not_Suc = standard (Suc_not_Zero RS not_sym);
+bind_thm ("Zero_not_Suc", (Suc_not_Zero RS not_sym));
 
-val Suc_neq_Zero = standard (Suc_not_Zero RS notE);
+bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
 val Zero_neq_Suc = sym RS Suc_neq_Zero;
 
 (** Injectiveness of Suc **)
@@ -158,7 +158,7 @@
 
 (*** nat_rec -- by wf recursion on pred_nat ***)
 
-val nat_rec_unfold = standard (wf_pred_nat RS (nat_rec_def RS def_wfrec));
+bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec)));
 
 (** conversion rules **)
 
@@ -221,7 +221,7 @@
 qed "less_not_sym";
 
 (* [| n<m; m<n |] ==> R *)
-val less_asym = standard (less_not_sym RS notE);
+bind_thm ("less_asym", (less_not_sym RS notE));
 
 goalw Nat.thy [less_def] "~ n<(n::nat)";
 by (rtac notI 1);
@@ -229,7 +229,7 @@
 qed "less_not_refl";
 
 (* n<n ==> R *)
-val less_anti_refl = standard (less_not_refl RS notE);
+bind_thm ("less_anti_refl", (less_not_refl RS notE));
 
 goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
 by(fast_tac (HOL_cs addEs [less_anti_refl]) 1);
@@ -252,7 +252,7 @@
 qed "not_less0";
 
 (* n<0 ==> R *)
-val less_zeroE = standard (not_less0 RS notE);
+bind_thm ("less_zeroE", (not_less0 RS notE));
 
 val [major,less,eq] = goal Nat.thy
     "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";