--- a/src/HOL/Integ/NatSimprocs.thy	Thu Apr 26 13:33:07 2007 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy	Thu Apr 26 13:33:09 2007 +0200
@@ -383,10 +383,9 @@
   "[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)"
   by (unfold dvd_def) auto
 
-ML
-{*
-val divide_minus1 = thm "divide_minus1";
-val minus1_divide = thm "minus1_divide";
+ML {*
+val divide_minus1 = @{thm divide_minus1};
+val minus1_divide = @{thm minus1_divide};
 *}
 
 end