src/Provers/classical.ML
changeset 32952 aeb1e44fbc19
parent 32863 5e8cef567042
child 32960 69916a850301
equal deleted inserted replaced
32951:83392f9d303f 32952:aeb1e44fbc19
   936     val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
   936     val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
   937     val rules = rules1 @ rules2 @ rules3 @ rules4;
   937     val rules = rules1 @ rules2 @ rules3 @ rules4;
   938     val ruleq = Drule.multi_resolves facts rules;
   938     val ruleq = Drule.multi_resolves facts rules;
   939   in
   939   in
   940     Method.trace ctxt rules;
   940     Method.trace ctxt rules;
   941     fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
   941     fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq
   942   end)
   942   end)
   943   THEN_ALL_NEW Goal.norm_hhf_tac;
   943   THEN_ALL_NEW Goal.norm_hhf_tac;
   944 
   944 
   945 in
   945 in
   946 
   946