changeset 19823 | 9e4573eaacb3 |
parent 19481 | a6205c6203ea |
child 20044 | 92cc2f4c7335 |
--- a/src/HOL/arith_data.ML Thu Jun 08 07:38:55 2006 +0200 +++ b/src/HOL/arith_data.ML Thu Jun 08 13:49:39 2006 +0200 @@ -494,7 +494,7 @@ *) fun raw_arith_tac ex i st = refute_tac (K true) - (REPEAT o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st)))) + (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st)))) (* (REPEAT o (fn i =>(split_tac (#splits (ArithTheoryData.get(Thm.theory_of_thm st))) i) THEN (simp_tac comp_ss i))) *)