Fixed bug in Pretype.sml for Poly/ML version 5.5, regarding "before".

Line 2442 and following:

  in (unify' n c1 c2 t1 t2 >>
      do_ho_matches unify1 unify1_le) e
     before end_homs()
  end

caused a type error with Poly/ML version 5.5. This is a difference from
Poly/ML version 5.3.

This bug was reported by Prof. Robert Solovay in an email.