diff -r f7aeff3e9e1e -r e6d7b77a0574 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Nov 07 17:48:25 2000 +0100
+++ b/src/Pure/tactic.ML	Tue Nov 07 17:50:21 2000 +0100
@@ -482,8 +482,8 @@
 val simple_prover =
   result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));
 
-val rewrite_rule = Drule.rewrite_rule_aux simple_prover;
-val rewrite_goals_rule = Drule.rewrite_goals_rule_aux simple_prover;
+val rewrite_rule = MetaSimplifier.rewrite_rule_aux simple_prover;
+val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
 
 
 (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)