# HG changeset patch
# User chaieb
# Date 1149768523 -7200
# Node ID bb53575366217e261fe2286de53f232953b83622
# Parent  fafceecebef002c7391ef7258cc722ae1f68d9a0
Splitting order changed.

diff -r fafceecebef0 -r bb5357536621 src/HOL/Real/ferrante_rackoff.ML
--- a/src/HOL/Real/ferrante_rackoff.ML	Thu Jun 08 13:49:53 2006 +0200
+++ b/src/HOL/Real/ferrante_rackoff.ML	Thu Jun 08 14:08:43 2006 +0200
@@ -79,7 +79,10 @@
 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
 
 
-fun ferrack_tac q i = ObjectLogic.atomize_tac i THEN (fn st =>
+fun ferrack_tac q i = 
+    (ObjectLogic.atomize_tac i) 
+	THEN (REPEAT_DETERM (split_tac [split_min, split_max,abs_split] i))
+	THEN (fn st =>
   let
     val g = List.nth (prems_of st, i - 1)
     val sg = sign_of_thm st
@@ -92,8 +95,7 @@
     val ct = cterm_of sg (HOLogic.mk_Trueprop t)
     (* Theorem for the nat --> int transformation *)
     val pre_thm = Seq.hd (EVERY
-      [simp_tac simpset0 1,
-       TRY (simp_tac simpset3 1), TRY (simp_tac context_ss 1)]
+      [simp_tac simpset0 1, TRY (simp_tac context_ss 1)]
       (trivial ct))
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)