src/HOL/Decision_Procs/commutative_ring_tac.ML
changeset 46708 b138dee7bed3
parent 44121 44adaa6db327
child 47432 e1576d13e933
     1.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Mon Feb 27 15:42:07 2012 +0100
     1.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Mon Feb 27 15:48:02 2012 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4      val norm_eq_th =
     1.5        simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
     1.6    in
     1.7 -    cut_rules_tac [norm_eq_th] i
     1.8 +    cut_tac norm_eq_th i
     1.9      THEN (simp_tac cring_ss i)
    1.10      THEN (simp_tac cring_ss i)
    1.11    end);