src/HOL/Word/Word.thy

       full_simp_tac (uint_arith_simpset ctxt) 1,
       ALLGOALS (full_simp_tac
         (put_simpset HOL_ss ctxt
           |> fold Splitter.add_split @{thms uint_splits}
           |> fold Simplifier.add_cong @{thms power_False_cong})),
-      rewrite_goals_tac @{thms word_size}, 
+      rewrite_goals_tac ctxt @{thms word_size}, 
       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
                          REPEAT (etac conjE n) THEN
                          REPEAT (dtac @{thm word_of_int_inverse} n 
                                  THEN atac n 
                                  THEN atac n)),

       full_simp_tac (unat_arith_simpset ctxt) 1,
       ALLGOALS (full_simp_tac
         (put_simpset HOL_ss ctxt
           |> fold Splitter.add_split @{thms unat_splits}
           |> fold Simplifier.add_cong @{thms power_False_cong})),
-      rewrite_goals_tac @{thms word_size}, 
+      rewrite_goals_tac ctxt @{thms word_size}, 
       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
                          REPEAT (etac conjE n) THEN
                          REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),
       TRYALL arith_tac' ] 
   end