src/Pure/tactic.ML
changeset 10415 e6d7b77a0574
parent 10347 c0cfc4ac12e2
child 10444 2dfa19236768
     1.1 --- a/src/Pure/tactic.ML	Tue Nov 07 17:48:25 2000 +0100
     1.2 +++ b/src/Pure/tactic.ML	Tue Nov 07 17:50:21 2000 +0100
     1.3 @@ -482,8 +482,8 @@
     1.4  val simple_prover =
     1.5    result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));
     1.6  
     1.7 -val rewrite_rule = Drule.rewrite_rule_aux simple_prover;
     1.8 -val rewrite_goals_rule = Drule.rewrite_goals_rule_aux simple_prover;
     1.9 +val rewrite_rule = MetaSimplifier.rewrite_rule_aux simple_prover;
    1.10 +val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
    1.11  
    1.12  
    1.13  (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)