src/HOL/arith_data.ML
changeset 10906 de95ba2760fe
parent 10766 ace2ba2d4fd1
child 11334 a16eaf2a1edd
     1.1 --- a/src/HOL/arith_data.ML	Tue Jan 16 00:27:37 2001 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Tue Jan 16 00:28:50 2001 +0100
     1.3 @@ -407,8 +407,6 @@
     1.4  *)
     1.5  local
     1.6  
     1.7 -val atomize_tac = Method.atomize_tac (thms "atomize'");
     1.8 -
     1.9  fun raw_arith_tac i st =
    1.10    refute_tac (K true) (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
    1.11               ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i st;