src/HOL/Algebra/abstract/Ring2.thy

--- a/src/HOL/Algebra/abstract/Ring2.thy	Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Sat Jul 21 23:25:00 2007 +0200
@@ -495,7 +495,7 @@
 (* fields are integral domains *)
 
 lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
-  apply (tactic "Step_tac 1")
+  apply (tactic "step_tac @{claset} 1")
   apply (rule_tac a = " (a*b) * inverse b" in box_equals)
     apply (rule_tac [3] refl)
    prefer 2