--- a/src/HOL/Word/Word.thy Mon Mar 09 11:21:00 2015 +0100
+++ b/src/HOL/Word/Word.thy Mon Mar 09 11:32:32 2015 +0100
@@ -1551,7 +1551,7 @@
fun uint_arith_tacs ctxt =
let
fun arith_tac' n t =
- Arith_Data.verbose_arith_tac ctxt n t
+ Arith_Data.arith_tac ctxt n t
handle Cooper.COOPER _ => Seq.empty;
in
[ clarify_tac ctxt 1,
@@ -2053,7 +2053,7 @@
fun unat_arith_tacs ctxt =
let
fun arith_tac' n t =
- Arith_Data.verbose_arith_tac ctxt n t
+ Arith_Data.arith_tac ctxt n t
handle Cooper.COOPER _ => Seq.empty;
in
[ clarify_tac ctxt 1,