[isabelle] found it



OK, I think PolyML.commit() does the job I want.  Sorry to bother.

Sean





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.