diff -r 4d0545e93c0d -r c533bc92e882 Arith.ML
--- a/Arith.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/Arith.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -189,7 +189,7 @@
 qed "diffs0_imp_equal_lemma";
 
 (*  [| m-n = 0;  n-m = 0 |] ==> m=n  *)
-val diffs0_imp_equal = standard (diffs0_imp_equal_lemma RS mp RS mp);
+bind_thm ("diffs0_imp_equal", (diffs0_imp_equal_lemma RS mp RS mp));
 
 val [prem] = goal Arith.thy "m<n ==> 0<n-m";
 by (rtac (prem RS rev_mp) 1);
@@ -235,8 +235,8 @@
 by (rtac le_add2 1);
 qed "le_add1";
 
-val less_add_Suc1 = standard (lessI RS (le_add1 RS le_less_trans));
-val less_add_Suc2 = standard (lessI RS (le_add2 RS le_less_trans));
+bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
+bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
 
 goal Arith.thy "m+k<=n --> m<=(n::nat)";
 by (nat_ind_tac "k" 1);