diff -r 9981199bf865 -r 1f3b832c90c1 src/HOL/ex/coopertac.ML --- a/src/HOL/ex/coopertac.ML Wed Jun 13 00:02:06 2007 +0200 +++ b/src/HOL/ex/coopertac.ML Wed Jun 13 03:28:21 2007 +0200 @@ -92,15 +92,15 @@ (* Simp rules for changing (n::int) to int n *) val simpset1 = HOL_basic_ss addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym) - [int_int_eq, zle_int, zless_int, zadd_int, zmult_int] + [@{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}] addsplits [zdiff_int_split] (*simp rules for elimination of int n*) val simpset2 = HOL_basic_ss - addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1] - addcongs [conj_le_cong, imp_le_cong] + addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}] + addcongs [@{thm conj_le_cong}, @{thm imp_le_cong}] (* simp rules for elimination of abs *) - val simpset3 = HOL_basic_ss addsplits [abs_split] + val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}] val ct = cterm_of thy (HOLogic.mk_Trueprop t) (* Theorem for the nat --> int transformation *) val pre_thm = Seq.hd (EVERY