# HG changeset patch
# User haftmann
# Date 1241773151 -7200
# Node ID ee1ebd405a37e880d5a862dbdbe61e08de16c7ca
# Parent  d47fa1db1820f950020a532c5201e24f71020d07
dropped legacy ml theorem binding

diff -r d47fa1db1820 -r ee1ebd405a37 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri May 08 09:48:54 2009 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri May 08 10:59:11 2009 +0200
@@ -83,7 +83,7 @@
       addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
     (* 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)
+      addsimps [@{thm nat_number_of_def}, zdvd_int] @ map (fn r => r RS sym)
         [@{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*)