src/Pure/Isar/local_defs.ML

         val frees = Term.fold_aterms (fn Free (x, _) =>
           if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop [];
       in
         Goal.prove ctxt' frees [] prop (K (ALLGOALS
           (meta_rewrite_tac ctxt' THEN'
-            Tactic.rewrite_goal_tac [def] THEN'
+            Goal.rewrite_goal_tac [def] THEN'
             Tactic.resolve_tac [Drule.reflexive_thm])))
         handle ERROR msg => cat_error msg "Failed to prove definitional specification."
       end;
   in (((c, T), rhs), prove) end;