src/Tools/isac/BridgeLibisabelle/datatypes.sml
changeset 60649 b2ff1902420f
parent 60642 33977a136810
child 60664 ed6f9e67349d
     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" ^