equal
deleted
inserted
replaced
639 EXCEPT theory hierarchy ... compare 'fun keref2xml' *) |
639 EXCEPT theory hierarchy ... compare 'fun keref2xml' *) |
640 fun pblID2guh pblID = (((#guh o get_pbt) pblID) |
640 fun pblID2guh pblID = (((#guh o get_pbt) pblID) |
641 handle _ => error ("pblID2guh: not for \"" ^ strs2str' pblID ^ "\"")); |
641 handle _ => error ("pblID2guh: not for \"" ^ strs2str' pblID ^ "\"")); |
642 fun metID2guh metID = (((#guh o get_met) metID) |
642 fun metID2guh metID = (((#guh o get_met) metID) |
643 handle _ => error ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\"")); |
643 handle _ => error ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\"")); |
644 fun kestoreID2guh Pbl_ kestoreID = pblID2guh kestoreID |
644 fun kestoreID2guh Celem.Pbl_ kestoreID = pblID2guh kestoreID |
645 | kestoreID2guh Met_ kestoreID = metID2guh kestoreID |
645 | kestoreID2guh Celem.Met_ kestoreID = metID2guh kestoreID |
646 | kestoreID2guh ketype kestoreID = |
646 | kestoreID2guh ketype kestoreID = |
647 error ("kestoreID2guh: \"" ^ Celem.ketype2str ketype ^ "\" not for \"" ^ strs2str' kestoreID ^ "\""); |
647 error ("kestoreID2guh: \"" ^ Celem.ketype2str ketype ^ "\" not for \"" ^ strs2str' kestoreID ^ "\""); |
648 |
648 |
649 fun show_pblguhs () = (* for tests *) |
649 fun show_pblguhs () = (* for tests *) |
650 (tracing o strs2str o (map Celem.linefeed)) (Celem.coll_pblguhs (get_ptyps ())) |
650 (tracing o strs2str o (map Celem.linefeed)) (Celem.coll_pblguhs (get_ptyps ())) |