| changeset 24078 | 04b28c723d43 |
| parent 23315 | df3a7e9ebadb |
| child 24110 | 4ab3084e311c |
--- 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