--- a/src/HOL/Hyperreal/Lim.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Wed Aug 30 03:19:08 2006 +0200
@@ -2239,7 +2239,7 @@
thus ?thesis by simp
qed
-ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *}
+ML {* fast_arith_split_limit := 0; *} (* FIXME *)
lemma LIMSEQ_SEQ_conv2:
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
@@ -2321,7 +2321,7 @@
ultimately show False by simp
qed
-ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
+ML {* fast_arith_split_limit := 9; *} (* FIXME *)
lemma LIMSEQ_SEQ_conv:
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = (X -- a --> L)"