1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Jan 11 06:06:12 2023 +0100
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Jan 11 09:23:18 2023 +0100
1.3 @@ -159,7 +159,7 @@
1.4 map xml_of_sub (Tactic.subst_adapt_to_type (ThyC.id_to_ctxt "Isac_Knowledge") subs))
1.5 fun xml_of_sube sube =
1.6 XML.Elem (("SUBSTITUTION", []),
1.7 - map xml_of_sub (Subst.T_from_string_eqs (ThyC.get_theory "Isac_Knowledge") sube))
1.8 + map xml_of_sub (Subst.T_from_string_eqs (Know_Store.get_via_last_thy "Isac_Knowledge") sube))
1.9
1.10 fun thm''2xml j (thm : thm) =
1.11 indt j ^ "<THEOREM>\n" ^