diff -r 958cc116d03b -r e19d5b459a61 src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Fri Mar 13 19:10:46 2009 +0100 +++ b/src/HOL/Word/WordArith.thy Fri Mar 13 19:53:09 2009 +0100 @@ -530,7 +530,7 @@ *} 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" @@ -1086,7 +1086,7 @@ *} 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: