--- a/src/HOL/HoareParallel/Graph.thy Tue Jul 31 00:56:31 2007 +0200
+++ b/src/HOL/HoareParallel/Graph.thy Tue Jul 31 00:56:31 2007 +0200
@@ -173,9 +173,9 @@
prefer 2 apply arith
apply(drule_tac n = "Suc nata" in Compl_lemma)
apply clarify
- ML {* fast_arith_split_limit := 0; *} (*FIXME*)
+ using [[option fast_arith_split_limit = 0]]
apply force
- ML {* fast_arith_split_limit := 9; *} (*FIXME*)
+ using [[option fast_arith_split_limit = 9]]
apply(drule leI)
apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
apply(erule_tac x = "m - (Suc nata)" in allE)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Jul 31 00:56:31 2007 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Jul 31 00:56:31 2007 +0200
@@ -454,10 +454,9 @@
apply (simp add: max_of_list_def)
apply (induct xs)
apply simp
-ML {* fast_arith_split_limit := 0; *} (* FIXME *)
+using [[option fast_arith_split_limit = 0]]
apply simp
apply arith
-ML {* fast_arith_split_limit := 9; *} (* FIXME *)
done