dropped Nat.ML legacy bindings
authorhaftmann
Fri, 20 Jul 2007 14:28:05 +0200 (2007-07-20)
changeset 23880 64b9806e160b
parent 23879 4776af8be741
child 23881 851c74f1bb69
dropped Nat.ML legacy bindings
src/HOL/Complex/ex/mirtac.ML
src/HOL/HoareParallel/Mul_Gar_Coll.thy
src/HOL/Nat.ML
src/HOL/Tools/Groebner_Basis/normalizer.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/W0/W0.thy
src/HOL/ex/coopertac.ML
--- a/src/HOL/Complex/ex/mirtac.ML	Fri Jul 20 14:28:01 2007 +0200
+++ b/src/HOL/Complex/ex/mirtac.ML	Fri Jul 20 14:28:05 2007 +0200
@@ -102,7 +102,7 @@
 				  @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
 				  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
 				  @{thm "Suc_plus1"}]
-			addsimps add_ac
+			addsimps @{thms add_ac}
 			addsimprocs [cancel_div_mod_proc]
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Fri Jul 20 14:28:01 2007 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Fri Jul 20 14:28:05 2007 +0200
@@ -1213,7 +1213,7 @@
 --{* 47 subgoals left *}
 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
 --{* 41 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (claset(),simpset() addsimps [thm "Queue_def", @{thm less_Suc_eq_le}, thm "le_length_filter_update"])]) *})
 --{* 35 subgoals left *}
 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
 --{* 31 subgoals left *}
@@ -1221,7 +1221,7 @@
 --{* 29 subgoals left *}
 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
 --{* 25 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (claset(),simpset() addsimps [thm "Queue_def", @{thm less_Suc_eq_le}, thm "le_length_filter_update"])]) *})
 --{* 10 subgoals left *}
 apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+
 done
--- a/src/HOL/Nat.ML	Fri Jul 20 14:28:01 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,225 +0,0 @@
-(*  Title:      HOL/Nat.ML
-    ID:         $Id$
-*)
-
-(** legacy ML bindings **)
-
-structure nat =
-struct
-  val distinct = thms "nat.distinct";
-  val inject = thms "nat.inject";
-  val exhaust = thm "nat.exhaust";
-  val cases = thms "nat.cases";
-  val split = thm "nat.split";
-  val split_asm = thm "nat.split_asm";
-  val induct = thm "nat.induct";
-  val recs = thms "nat.recs";
-  val simps = thms "nat.simps";
-end;
-
-val Least_Suc = thm "Least_Suc";
-val Least_Suc2 = thm "Least_Suc2";
-val One_nat_def = thm "One_nat_def";
-val Suc_Suc_eq = thm "Suc_Suc_eq";
-val Suc_def = thm "Suc_def";
-val Suc_diff_diff = thm "Suc_diff_diff";
-val Suc_diff_le = thm "Suc_diff_le";
-val Suc_inject = thm "Suc_inject";
-val Suc_leD = thm "Suc_leD";
-val Suc_leI = thm "Suc_leI";
-val Suc_le_D = thm "Suc_le_D";
-val Suc_le_eq = thm "Suc_le_eq";
-val Suc_le_lessD = thm "Suc_le_lessD";
-val Suc_le_mono = thm "Suc_le_mono";
-val Suc_lessD = thm "Suc_lessD";
-val Suc_lessE = thm "Suc_lessE";
-val Suc_lessI = thm "Suc_lessI";
-val Suc_less_SucD = thm "Suc_less_SucD";
-val Suc_less_eq = thm "Suc_less_eq";
-val Suc_mono = thm "Suc_mono";
-val Suc_mult_cancel1 = thm "Suc_mult_cancel1";
-val Suc_mult_le_cancel1 = thm "Suc_mult_le_cancel1";
-val Suc_mult_less_cancel1 = thm "Suc_mult_less_cancel1";
-val Suc_n_not_le_n = thm "Suc_n_not_le_n";
-val Suc_n_not_n = thm "Suc_n_not_n";
-val Suc_neq_Zero = thm "Suc_neq_Zero";
-val Suc_not_Zero = thm "Suc_not_Zero";
-val Suc_pred = thm "Suc_pred";
-val Zero_nat_def = thm "Zero_nat_def";
-val Zero_neq_Suc = thm "Zero_neq_Suc";
-val Zero_not_Suc = thm "Zero_not_Suc";
-val add_0 = thm "add_0";
-val add_0_right = thm "add_0_right";
-val add_Suc = thm "add_Suc";
-val add_Suc_right = thm "add_Suc_right";
-val add_ac = thms "add_ac";
-val add_assoc = thm "add_assoc";
-val add_commute = thm "add_commute";
-val add_diff_inverse = thm "add_diff_inverse";
-val add_eq_self_zero = thm "add_eq_self_zero";
-val add_gr_0 = thm "add_gr_0";
-val add_is_0 = thm "add_is_0";
-val add_is_1 = thm "add_is_1";
-val add_leD1 = thm "add_leD1";
-val add_leD2 = thm "add_leD2";
-val add_leE = thm "add_leE";
-val add_le_mono = thm "add_le_mono";
-val add_le_mono1 = thm "add_le_mono1";
-val nat_add_left_cancel = thm "nat_add_left_cancel";
-val nat_add_left_cancel_le = thm "nat_add_left_cancel_le";
-val nat_add_left_cancel_less = thm "nat_add_left_cancel_less";
-val add_left_commute = thm "add_left_commute";
-val add_lessD1 = thm "add_lessD1";
-val add_less_mono = thm "add_less_mono";
-val add_less_mono1 = thm "add_less_mono1";
-val add_mult_distrib = thm "add_mult_distrib";
-val add_mult_distrib2 = thm "add_mult_distrib2";
-val nat_add_right_cancel = thm "nat_add_right_cancel";
-val def_nat_rec_0 = thm "def_nat_rec_0";
-val def_nat_rec_Suc = thm "def_nat_rec_Suc";
-val diff_0 = thm "diff_0";
-val diff_0_eq_0 = thm "diff_0_eq_0";
-val diff_Suc = thm "diff_Suc";
-val diff_Suc_Suc = thm "diff_Suc_Suc";
-val diff_Suc_less = thm "diff_Suc_less";
-val diff_add_0 = thm "diff_add_0";
-val diff_add_assoc = thm "diff_add_assoc";
-val diff_add_assoc2 = thm "diff_add_assoc2";
-val diff_add_inverse = thm "diff_add_inverse";
-val diff_add_inverse2 = thm "diff_add_inverse2";
-val diff_cancel = thm "diff_cancel";
-val diff_cancel2 = thm "diff_cancel2";
-val diff_commute = thm "diff_commute";
-val diff_diff_left = thm "diff_diff_left";
-val diff_induct = thm "diff_induct";
-val diff_is_0_eq = thm "diff_is_0_eq";
-val diff_le_self = thm "diff_le_self";
-val diff_less_Suc = thm "diff_less_Suc";
-val diff_mult_distrib = thm "diff_mult_distrib"; 
-val diff_mult_distrib2 = thm "diff_mult_distrib2"; 
-val diff_self_eq_0 = thm "diff_self_eq_0";
-val eq_imp_le = thm "eq_imp_le";
-val gr0I = thm "gr0I";
-val gr0_conv_Suc = thm "gr0_conv_Suc";
-val gr_implies_not0 = thm "gr_implies_not0";
-val inj_Suc = thm "inj_Suc";
-val le0 = thm "le0";
-val le_0_eq = thm "le_0_eq";
-val le_SucE = thm "le_SucE";
-val le_SucI = thm "le_SucI";
-val le_Suc_eq = thm "le_Suc_eq";
-val le_add1 = thm "le_add1";
-val le_add2 = thm "le_add2";
-val le_add_diff_inverse = thm "le_add_diff_inverse";
-val le_add_diff_inverse2 = thm "le_add_diff_inverse2";
-val le_anti_sym = thm "le_anti_sym";
-val le_def = thm "le_def";
-val le_eq_less_or_eq = thm "le_eq_less_or_eq";
-val le_imp_diff_is_add = thm "le_imp_diff_is_add";
-val le_imp_less_Suc = thm "le_imp_less_Suc";
-val le_imp_less_or_eq = thm "le_imp_less_or_eq";
-val le_less_trans = thm "le_less_trans";
-val le_neq_implies_less = thm "le_neq_implies_less";
-val le_refl = thm "le_refl";
-val le_simps = thms "le_simps";
-val le_trans = thm "le_trans";
-val lessE = thm "lessE";
-val lessI = thm "lessI";
-val less_Suc0 = thm "less_Suc0";
-val less_SucE = thm "less_SucE";
-val less_SucI = thm "less_SucI";
-val less_Suc_eq = thm "less_Suc_eq";
-val less_Suc_eq_0_disj = thm "less_Suc_eq_0_disj";
-val less_Suc_eq_le = thm "less_Suc_eq_le";
-val less_add_Suc1 = thm "less_add_Suc1";
-val less_add_Suc2 = thm "less_add_Suc2";
-val less_add_eq_less = thm "less_add_eq_less";
-val less_asym = thm "less_asym";
-val less_def = thm "less_def";
-val less_eq = thm "less_eq";
-val less_iff_Suc_add = thm "less_iff_Suc_add";
-val less_imp_Suc_add = thm "less_imp_Suc_add";
-val less_imp_add_positive = thm "less_imp_add_positive";
-val less_imp_diff_less = thm "less_imp_diff_less";
-val less_imp_le = thm "less_imp_le";
-val less_irrefl = thm "less_irrefl";
-val less_le_trans = thm "less_le_trans";
-val less_linear = thm "less_linear";
-val less_mono_imp_le_mono = thm "less_mono_imp_le_mono";
-val less_not_refl = thm "less_not_refl";
-val less_not_refl2 = thm "less_not_refl2";
-val less_not_refl3 = thm "less_not_refl3";
-val less_not_sym = thm "less_not_sym";
-val less_one = thm "less_one";
-val less_or_eq_imp_le = thm "less_or_eq_imp_le";
-val less_trans = thm "less_trans";
-val less_trans_Suc = thm "less_trans_Suc";
-val less_zeroE = thm "less_zeroE";
-val max_0L = thm "max_0L";
-val max_0R = thm "max_0R";
-val max_Suc_Suc = thm "max_Suc_Suc";
-val min_0L = thm "min_0L";
-val min_0R = thm "min_0R";
-val min_Suc_Suc = thm "min_Suc_Suc";
-val mult_0 = thm "mult_0";
-val mult_0_right = thm "mult_0_right";
-val mult_1 = thm "mult_1";
-val mult_1_right = thm "mult_1_right";
-val mult_Suc = thm "mult_Suc";
-val mult_Suc_right = thm "mult_Suc_right";
-val mult_ac = thms "mult_ac";
-val mult_assoc = thm "mult_assoc";
-val mult_cancel1 = thm "mult_cancel1";
-val mult_cancel2 = thm "mult_cancel2";
-val mult_commute = thm "mult_commute";
-val mult_eq_1_iff = thm "mult_eq_1_iff";
-val mult_eq_self_implies_10 = thm "mult_eq_self_implies_10";
-val mult_is_0 = thm "mult_is_0";
-val mult_le_cancel1 = thm "mult_le_cancel1";
-val mult_le_cancel2 = thm "mult_le_cancel2";
-val mult_le_mono = thm "mult_le_mono";
-val mult_le_mono1 = thm "mult_le_mono1";
-val mult_le_mono2 = thm "mult_le_mono2";
-val mult_left_commute = thm "mult_left_commute";
-val mult_less_cancel1 = thm "mult_less_cancel1";
-val mult_less_cancel2 = thm "mult_less_cancel2";
-val mult_less_mono1 = thm "mult_less_mono1";
-val mult_less_mono2 = thm "mult_less_mono2";
-val n_not_Suc_n = thm "n_not_Suc_n";
-val nat_distrib = thms "nat_distrib";
-val nat_induct = thm "nat_induct";
-val nat_induct2 = thm "nat_induct2";
-val nat_le_linear = thm "nat_le_linear";
-val nat_less_cases = thm "nat_less_cases";
-val nat_less_induct = thm "nat_less_induct";
-val nat_less_le = thm "nat_less_le";
-val nat_neq_iff = thm "nat_neq_iff";
-val nat_not_singleton = thm "nat_not_singleton";
-val neq0_conv = thm "neq0_conv";
-val not0_implies_Suc = thm "not0_implies_Suc";
-val not_add_less1 = thm "not_add_less1";
-val not_add_less2 = thm "not_add_less2";
-val not_gr0 = thm "not_gr0";
-val not_leE = thm "not_leE";
-val not_less0 = thm "not_less0";
-val not_less_eq = thm "not_less_eq";
-val not_less_less_Suc_eq = thm "not_less_less_Suc_eq";
-val not_less_simps = thms "not_less_simps";
-val one_eq_mult_iff = thm "one_eq_mult_iff";
-val one_is_add = thm "one_is_add";
-val one_le_mult_iff = thm "one_le_mult_iff";
-val one_reorient = thm "one_reorient";
-val pred_nat_def = thm "pred_nat_def";
-val trans_le_add1 = thm "trans_le_add1";
-val trans_le_add2 = thm "trans_le_add2";
-val trans_less_add1 = thm "trans_less_add1";
-val trans_less_add2 = thm "trans_less_add2";
-val wf_less = thm "wf_less";
-val wf_pred_nat = thm "wf_pred_nat";
-val zero_induct = thm "zero_induct";
-val zero_induct_lemma = thm "zero_induct_lemma";
-val zero_less_Suc = thm "zero_less_Suc";
-val zero_less_diff = thm "zero_less_diff";
-val zero_less_mult_iff = thm "zero_less_mult_iff";
-val zero_reorient = thm "zero_reorient";
-val linorder_neqE_nat = thm "linorder_neqE_nat";
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Fri Jul 20 14:28:01 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Fri Jul 20 14:28:05 2007 +0200
@@ -39,7 +39,7 @@
   (Simplifier.rewrite 
     (HOL_basic_ss 
        addsimps arith_simps @ natarith @ rel_simps
-             @ [if_False, if_True, add_0, add_Suc, add_number_of_left, Suc_eq_add_numeral_1]
+             @ [if_False, if_True, @{thm add_0}, @{thm add_Suc}, add_number_of_left, Suc_eq_add_numeral_1]
              @ map (fn th => th RS sym) numerals));
 
 val nat_mul_conv = nat_add_conv;
@@ -590,7 +590,7 @@
 
 val nat_arith = @{thms "nat_arith"};
 val nat_exp_ss = HOL_basic_ss addsimps (nat_number @ nat_arith @ arith_simps @ rel_simps)
-                              addsimps [Let_def, if_False, if_True, add_0, add_Suc];
+                              addsimps [Let_def, if_False, if_True, @{thm add_0}, @{thm add_Suc}];
 
 fun simple_cterm_ord t u = Term.term_ord (term_of t, term_of u) = LESS;
 fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom}, 
--- a/src/HOL/Tools/Qelim/presburger.ML	Fri Jul 20 14:28:01 2007 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Fri Jul 20 14:28:05 2007 +0200
@@ -115,7 +115,7 @@
      @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
      @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, 
      @{thm "mod_1"}, @{thm "Suc_plus1"}]
-  @ add_ac
+  @ @{thms add_ac}
  addsimprocs [cancel_div_mod_proc]
  val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
      [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
--- a/src/HOL/Tools/TFL/post.ML	Fri Jul 20 14:28:01 2007 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Fri Jul 20 14:28:05 2007 +0200
@@ -69,7 +69,7 @@
    {wf_tac     = REPEAT (ares_tac wfs 1),
     terminator = asm_simp_tac ss 1
                  THEN TRY (silent_arith_tac 1 ORELSE
-                           fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
+                           fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1),
     simplifier = Rules.simpl_conv ss []};
 
 
--- a/src/HOL/Tools/function_package/fundef_core.ML	Fri Jul 20 14:28:01 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Fri Jul 20 14:28:05 2007 +0200
@@ -93,19 +93,19 @@
 
 
 (* Theory dependencies. *)
-val Pair_inject = thm "Product_Type.Pair_inject";
+val Pair_inject = @{thm Product_Type.Pair_inject};
 
-val acc_induct_rule = thm "Accessible_Part.accp_induct_rule"
+val acc_induct_rule = @{thm Accessible_Part.accp_induct_rule};
 
-val ex1_implies_ex = thm "FunDef.fundef_ex1_existence"
-val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness"
-val ex1_implies_iff = thm "FunDef.fundef_ex1_iff"
+val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
+val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness};
+val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff};
 
-val acc_downward = thm "Accessible_Part.accp_downward"
-val accI = thm "Accessible_Part.accp.accI"
-val case_split = thm "HOL.case_split_thm"
-val fundef_default_value = thm "FunDef.fundef_default_value"
-val not_acc_down = thm "Accessible_Part.not_accp_down"
+val acc_downward = @{thm Accessible_Part.accp_downward};
+val accI = @{thm Accessible_Part.accp.accI};
+val case_split = @{thm HOL.case_split_thm};
+val fundef_default_value = @{thm FunDef.fundef_default_value};
+val not_acc_down = @{thm Accessible_Part.not_accp_down};
 
 
 
@@ -573,8 +573,7 @@
 (** Induction rule **)
 
 
-val acc_subset_induct = thm "Fun.predicate1I" RS
-  thm "Accessible_Part.accp_subset_induct"
+val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm Accessible_Part.accp_subset_induct}
 
 fun mk_partial_induct_rule thy globals R complete_thm clauses =
     let
@@ -704,9 +703,9 @@
 
 (** Termination rule **)
 
-val wf_induct_rule = thm "Wellfounded_Recursion.wfP_induct_rule";
-val wf_in_rel = thm "FunDef.wf_in_rel";
-val in_rel_def = thm "FunDef.in_rel_def";
+val wf_induct_rule = @{thm Wellfounded_Recursion.wfP_induct_rule};
+val wf_in_rel = @{thm FunDef.wf_in_rel};
+val in_rel_def = @{thm FunDef.in_rel_def};
 
 fun mk_nest_term_case thy globals R' ihyp clause =
     let
--- a/src/HOL/W0/W0.thy	Fri Jul 20 14:28:01 2007 +0200
+++ b/src/HOL/W0/W0.thy	Fri Jul 20 14:28:05 2007 +0200
@@ -210,7 +210,7 @@
   apply (unfold free_tv_subst cod_def dom_def)
   apply (tactic "safe_tac set_cs")
    apply (cut_tac m = m and n = n in less_linear)
-   apply (tactic "fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1")
+   apply (tactic "fast_tac (HOL_cs addSIs [@{thm less_or_eq_imp_le}]) 1")
   apply (cut_tac m = ma and n = n in less_linear)
   apply (fast intro!: less_or_eq_imp_le)
   done
@@ -618,7 +618,7 @@
   apply (tactic {* fast_tac (HOL_cs addDs [thm "mgu_free", thm "codD",
     thm "free_tv_subst_var" RS subsetD,
     thm "free_tv_app_subst_te" RS subsetD,
-    thm "free_tv_app_subst_tel" RS subsetD, less_le_trans, subsetD]
+    thm "free_tv_app_subst_tel" RS subsetD, @{thm less_le_trans}, subsetD]
     addSEs [UnE] addss (simpset() setSolver unsafe_solver)) 1 *})
       -- {* builtin arithmetic in simpset messes things up *}
   done
@@ -809,13 +809,13 @@
     apply (erule impE)
      prefer 2 apply (fastsimp simp add: new_tv_subst)
     apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
-      thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
+      thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *})
    apply (intro strip)
    apply (erule allE)+
    apply (erule impE)
     prefer 2 apply (fastsimp simp add: new_tv_subst)
    apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
-     thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
+     thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *})
   txt {* case @{text "App e1 e2"} *}
   apply (tactic {* simp_tac (simpset () setloop (split_inside_tac [thm "split_bind"])) 1 *})
   apply (intro strip)
@@ -891,7 +891,7 @@
    apply (intro strip)
    apply (subgoal_tac "TVar m # $s a = $s (TVar m # a)")
     apply (tactic {* asm_simp_tac (HOL_ss addsimps
-      [thm "new_tv_Suc_list", lessI RS less_imp_le RS thm "new_tv_subst_le"]) 1 *})
+      [thm "new_tv_Suc_list", @{thm lessI} RS @{thm less_imp_le} RS thm "new_tv_subst_le"]) 1 *})
     apply (erule conjE)
     apply (drule new_tv_not_free_tv [THEN not_free_impl_id])
     apply (simp (no_asm_simp))
--- a/src/HOL/ex/coopertac.ML	Fri Jul 20 14:28:01 2007 +0200
+++ b/src/HOL/ex/coopertac.ML	Fri Jul 20 14:28:05 2007 +0200
@@ -83,7 +83,7 @@
 				  @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
 				  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
 				  Suc_plus1]
-			addsimps add_ac
+			addsimps @{thms add_ac}
 			addsimprocs [cancel_div_mod_proc]
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]