bind_thms;

--- a/src/HOL/Arith.ML	Wed Sep 01 21:25:17 1999 +0200
+++ b/src/HOL/Arith.ML	Wed Sep 01 21:25:55 1999 +0200
@@ -74,7 +74,7 @@
 qed "add_left_commute";
 
 (*Addition is an AC-operator*)
-val add_ac = [add_assoc, add_commute, add_left_commute];
+bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
 
 Goal "(k + m = k + n) = (m=(n::nat))";
 by (induct_tac "k" 1);
@@ -329,7 +329,7 @@
 by (rtac (mult_commute RS arg_cong) 1);
 qed "mult_left_commute";
 
-val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
+bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
 
 Goal "(m*n = 0) = (m=0 | n=0)";
 by (induct_tac "m" 1);
@@ -1006,7 +1006,8 @@
 
 (* proof method setup *)
 
-val arith_method = Method.METHOD (fn facts => FIRSTGOAL (Method.same_tac facts THEN' arith_tac));
+val arith_method =
+  Method.METHOD (fn facts => FIRSTGOAL (Method.insert_tac facts THEN' arith_tac));
 
 val arith_setup =
  [Method.add_methods

--- a/src/HOL/Integ/IntDef.ML	Wed Sep 01 21:25:17 1999 +0200
+++ b/src/HOL/Integ/IntDef.ML	Wed Sep 01 21:25:55 1999 +0200
@@ -188,7 +188,7 @@
 qed "zadd_left_commute";
 
 (*Integer addition is an AC operator*)
-val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
+bind_thms ("zadd_ac", [zadd_assoc,zadd_commute,zadd_left_commute]);
 
 Goalw [int_def] "(int m) + (int n) = int (m + n)";
 by (simp_tac (simpset() addsimps [zadd]) 1);
@@ -325,7 +325,7 @@
 qed "zmult_left_commute";
 
 (*Integer multiplication is an AC operator*)
-val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
+bind_thms ("zmult_ac", [zmult_assoc, zmult_commute, zmult_left_commute]);
 
 Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
 by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);

--- a/src/HOL/Real/RealDef.ML	Wed Sep 01 21:25:17 1999 +0200
+++ b/src/HOL/Real/RealDef.ML	Wed Sep 01 21:25:55 1999 +0200
@@ -194,7 +194,7 @@
 qed "real_add_left_commute";
 
 (* real addition is an AC operator *)
-val real_add_ac = [real_add_assoc,real_add_commute,real_add_left_commute];
+bind_thms ("real_add_ac", [real_add_assoc,real_add_commute,real_add_left_commute]);
 
 Goalw [real_of_preal_def,real_zero_def] "0r + z = z";
 by (res_inst_tac [("z","z")] eq_Abs_real 1);
@@ -361,7 +361,7 @@
            rtac (real_mult_commute RS arg_cong) 1]);
 
 (* real multiplication is an AC operator *)
-val real_mult_ac = [real_mult_assoc, real_mult_commute, real_mult_left_commute];
+bind_thms ("real_mult_ac", [real_mult_assoc, real_mult_commute, real_mult_left_commute]);
 
 Goalw [real_one_def,pnat_one_def] "1r * z = z";
 by (res_inst_tac [("z","z")] eq_Abs_real 1);
@@ -880,7 +880,7 @@
 by (assume_tac 1);
 qed "real_leD";
 
-val real_leE = make_elim real_leD;
+bind_thm ("real_leE", make_elim real_leD);
 
 Goal "(~(w < z)) = (z <= (w::real))";
 by (blast_tac (claset() addSIs [real_leI,real_leD]) 1);