diff -r 9c8cc63714f4 -r 556ce89b7d41 src/HOL/HoareParallel/OG_Examples.thy
--- a/src/HOL/HoareParallel/OG_Examples.thy	Tue May 18 11:45:50 2004 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Wed May 19 11:21:19 2004 +0200
@@ -445,7 +445,9 @@
 apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
 --{* 33 subgoals left *}
 apply(tactic {* ALLGOALS Clarify_tac *})
-apply(tactic {* TRYALL arith_tac *})
+
+ML "set Presburger.trace"
+apply(tactic {* TRYALL simple_arith_tac *})
 --{* 10 subgoals left *}
 apply (force simp add:less_Suc_eq)
 apply(drule sym)