equal
deleted
inserted
replaced
568 |
568 |
569 fun ori2str ((i,vs,fi,t,ts):ori) = |
569 fun ori2str ((i,vs,fi,t,ts):ori) = |
570 "("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^ |
570 "("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^ |
571 (term2str t)^", "^((strs2str o (map term2str)) ts)^")"; |
571 (term2str t)^", "^((strs2str o (map term2str)) ts)^")"; |
572 val oris2str = |
572 val oris2str = |
573 let val s = !show_types |
573 let (*val s = !show_types |
574 val _ = show_types:= true |
574 val _ = show_types:= true*) |
575 val str = (strs2str' o (map (linefeed o ori2str))) |
575 val str = (strs2str' o (map (linefeed o ori2str))) |
576 val _ = show_types:= s |
576 (*val _ = show_types:= s*) |
577 in str end; |
577 in str end; |
578 |
578 |
579 (*.an or without leading integer.*) |
579 (*.an or without leading integer.*) |
580 type preori = (vats * |
580 type preori = (vats * |
581 string * |
581 string * |