Added functor f() = struct end to hide functors to save space.

Renamed insert_kbrl to insert_tagged_brl and exported it. Now subgoals_of_brl calls nprems_of, which is faster than length o prems_of.

Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.