src/HOL/Algebra/abstract/Ring2.thy

--- a/src/HOL/Algebra/abstract/Ring2.thy	Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Fri May 13 22:55:00 2011 +0200
@@ -466,7 +466,7 @@
 (* fields are integral domains *)
 
 lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
-  apply (tactic "step_tac @{claset} 1")
+  apply (tactic "step_tac @{context} 1")
   apply (rule_tac a = " (a*b) * inverse b" in box_equals)
     apply (rule_tac [3] refl)
    prefer 2