default rule step: norm_hhf_tac;

--- a/src/Provers/classical.ML	Sun Jan 29 19:23:40 2006 +0100
+++ b/src/Provers/classical.ML	Sun Jan 29 19:23:41 2006 +0100
@@ -1021,7 +1021,8 @@
   in
     Method.trace ctxt rules;
     fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
-  end);
+  end)
+  THEN_ALL_NEW Tactic.norm_hhf_tac;
 
 fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
   | rule_tac rules _ _ facts = Method.rule_tac rules facts;