1.1 --- a/src/Tools/isac/BridgeLibisabelle/present-tool.sml	Wed Jan 11 06:06:12 2023 +0100
     1.2 +++ b/src/Tools/isac/BridgeLibisabelle/present-tool.sml	Wed Jan 11 09:23:18 2023 +0100
     1.3 @@ -76,7 +76,8 @@
     1.4     EXCEPT theory hierarchy ... compare 'fun keref2xml'    *)
     1.5  fun pblID2guh ctxt pblID = (((#guh o (Problem.from_store ctxt)) pblID)
     1.6    handle ERROR _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));
     1.7 -fun metID2guh metID = (((#guh o MethodC.from_store ("Isac_Knowledge" |> ThyC.get_theory |> Proof_Context.init_global)) metID)
     1.8 +fun metID2guh metID =
     1.9 +  (((#guh o MethodC.from_store ("Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global)) metID)
    1.10    handle ERROR _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));
    1.11  fun kestoreID2guh ctxt Pbl_ kestoreID = pblID2guh ctxt kestoreID
    1.12    | kestoreID2guh _ Met_ kestoreID = metID2guh kestoreID