--- a/src/HOL/Word/WordArith.thy Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Word/WordArith.thy Mon Mar 23 19:01:16 2009 +0100
@@ -512,7 +512,7 @@
fun uint_arith_tacs ctxt =
let
- fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
+ fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
val cs = local_claset_of ctxt;
val ss = local_simpset_of ctxt;
in
@@ -1075,7 +1075,7 @@
fun unat_arith_tacs ctxt =
let
- fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
+ fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
val cs = local_claset_of ctxt;
val ss = local_simpset_of ctxt;
in