turned structure NetRules into general Item_Net, which is loaded earlier;

renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);

goal_tac: finish marked assumptions from left to right -- corresponds better with the strategy of etac, with significant performance gains in some situations;

eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly; tuned;

tuned aeconv: test plain aconv before expensive eta_contract;

substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);