Working towards HOL output.

UNIV and o_f are causing problems.