src/HOL/ex/Binary.thy
changeset 30510 4120fc59dd85
parent 26187 3e099fc47afd
child 30549 d2d7874648bd
--- a/src/HOL/ex/Binary.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/ex/Binary.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -174,7 +174,7 @@
 simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}
 
 method_setup binary_simp = {*
-  Method.no_args (Method.SIMPLE_METHOD'
+  Method.no_args (SIMPLE_METHOD'
     (full_simp_tac
       (HOL_basic_ss
         addsimps @{thms binary_simps}