# HG changeset patch
# User wenzelm
# Date 1138559021 -3600
# Node ID 7e94af77cfcee078e82d8a6e22e498e8dccce17f
# Parent  bead1a4e966b30a6dcdf306295c113ede1954734
default rule step: norm_hhf_tac;

diff -r bead1a4e966b -r 7e94af77cfce src/Provers/classical.ML
--- 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;