Make Feedback streams fns rather than outstreams

Allows a smidge more generality

INST_TT_HYPS - as INST_TY_TERM but also retuns hyps in the order
they are returned by hyp (original theorem)

needed so that irule will give new subgoals in predictable order
temporary change to Drule.INST_TY_TERM is for testing

Fix bug in Moscow ML version of LaTeX munger

Issue was that Moscow ML mungers start by executing the SML code in the
various theories that are built into them. This can cause warning
messages, and these warnings were written to standard out. This then
causes the output to be other than desired. (Standard out should only
contain the munged LaTeX source.)

There's code that runs before the lexing loop starts to switch HOL
warnings to standard error, but this is executed after the theories
load. So, yes, it would be nice if theory structures were side-effect
free, but we actually want theories to induce all sorts of side effects
as they load, and thus code needs to execute, and that code might cause
messages to go to standard out.

By contrast, in Poly/ML things are staged: the theories are loaded once
and put into the heap that is then executed to implement the munger's
lexing. This makes things more efficient of course, and also means that
warnings on theory loads are emitted when the munger is built, not when
it is run.

The fix in the Moscow ML world is to make the final munger executable
include an object file (warning_stream.uo) that sets the warning stream
appropriately. Because Moscow ML loads things in the order they appear
on the compilation command-line (to the extent that this is possible),
this is executed before the theories are executed, and all is well.