equal
deleted
inserted
replaced
74 |
74 |
75 (* make a guh from a reference to an element in the kestore; |
75 (* make a guh from a reference to an element in the kestore; |
76 EXCEPT theory hierarchy ... compare 'fun keref2xml' *) |
76 EXCEPT theory hierarchy ... compare 'fun keref2xml' *) |
77 fun pblID2guh ctxt pblID = (((#guh o (Problem.from_store ctxt)) pblID) |
77 fun pblID2guh ctxt pblID = (((#guh o (Problem.from_store ctxt)) pblID) |
78 handle ERROR _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\"")); |
78 handle ERROR _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\"")); |
79 fun metID2guh metID = (((#guh o MethodC.from_store ("Isac_Knowledge" |> ThyC.get_theory |> Proof_Context.init_global)) metID) |
79 fun metID2guh metID = |
|
80 (((#guh o MethodC.from_store ("Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global)) metID) |
80 handle ERROR _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\"")); |
81 handle ERROR _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\"")); |
81 fun kestoreID2guh ctxt Pbl_ kestoreID = pblID2guh ctxt kestoreID |
82 fun kestoreID2guh ctxt Pbl_ kestoreID = pblID2guh ctxt kestoreID |
82 | kestoreID2guh _ Met_ kestoreID = metID2guh kestoreID |
83 | kestoreID2guh _ Met_ kestoreID = metID2guh kestoreID |
83 | kestoreID2guh _ ketyp kestoreID = |
84 | kestoreID2guh _ ketyp kestoreID = |
84 raise ERROR ("kestoreID2guh: \"" ^ ketype2str ketyp ^ "\" not for \"" ^ strs2str' kestoreID ^ "\""); |
85 raise ERROR ("kestoreID2guh: \"" ^ ketype2str ketyp ^ "\" not for \"" ^ strs2str' kestoreID ^ "\""); |