src/HOL/Word/WordArith.thy

 
 fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt))
 *}
 
 method_setup uint_arith = 
-  "Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (uint_arith_tac ctxt 1))" 
+  "Method.ctxt_args (SIMPLE_METHOD' o uint_arith_tac)" 
   "solving word arithmetic via integers and arith"
 
 
 subsection "More on overflows and monotonicity"
 

 
 fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))
 *}
 
 method_setup unat_arith = 
-  "Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (unat_arith_tac ctxt 1))" 
+  "Method.ctxt_args (SIMPLE_METHOD' o unat_arith_tac)" 
   "solving word arithmetic via natural numbers and arith"
 
 lemma no_plus_overflow_unat_size: 
   "((x :: 'a :: len word) <= x + y) = (unat x + unat y < 2 ^ size x)" 
   unfolding word_size by unat_arith