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