--- a/src/HOL/ex/Arith_Examples.thy Fri Feb 19 09:35:18 2010 +0100
+++ b/src/HOL/ex/Arith_Examples.thy Fri Feb 19 11:49:44 2010 +0100
@@ -123,12 +123,12 @@
(* FIXME: need to replace 1 by its numeral representation *)
apply (subst numeral_1_eq_1 [symmetric])
(* FIXME: arith does not know about iszero *)
- apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
+ apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *})
oops
lemma "(i::int) mod 42 <= 41"
(* FIXME: arith does not know about iszero *)
- apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
+ apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *})
oops
lemma "-(i::int) * 1 = 0 ==> i = 0"