equal
deleted
inserted
replaced
364 *) |
364 *) |
365 type penv = (term (*err_*) |
365 type penv = (term (*err_*) |
366 * (term list) (*[#0, epsilon] 9.5.03 outcommented*) |
366 * (term list) (*[#0, epsilon] 9.5.03 outcommented*) |
367 ) list; |
367 ) list; |
368 fun pen2str thy (t, ts) = |
368 fun pen2str thy (t, ts) = |
369 pair2str(Sign.string_of_term (sign_of thy) t, |
369 pair2str(Syntax.string_of_term GOON (sign_of thy) t, |
370 (strs2str' o map (Sign.string_of_term (sign_of thy))) ts); |
370 (strs2str' o map (Sign.string_of_term (sign_of thy))) ts); |
371 fun penv2str thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv; |
371 fun penv2str thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv; |
372 |
372 |
373 (* |
373 (* |
374 9.5.03: still unused, but left for eventual future development*) |
374 9.5.03: still unused, but left for eventual future development*) |