| changeset 21687 | f689f729afab |
| parent 21646 | c07b5b0e8492 |
| child 21689 | 58abd6d8abd1 |
--- a/src/Provers/classical.ML Wed Dec 06 21:19:03 2006 +0100 +++ b/src/Provers/classical.ML Thu Dec 07 00:42:04 2006 +0100 @@ -1005,7 +1005,7 @@ Method.trace ctxt rules; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end) - THEN_ALL_NEW Tactic.norm_hhf_tac; + THEN_ALL_NEW Goal.norm_hhf_tac; fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts | rule_tac rules _ _ facts = Method.rule_tac rules facts;