src/HOL/Word/WordBitwise.thy

--- a/src/HOL/Word/WordBitwise.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Word/WordBitwise.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -518,7 +518,7 @@
       in
         try (fn () =>
           Goal.prove_internal ctxt [] prop 
-            (K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1
+            (K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1
                 ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
       end
   | _ => NONE;