src/Tools/isac/MathEngBasic/ctree-basic.sml
changeset 60649 b2ff1902420f
parent 60643 376a1629989e
child 60654 c2db35151fba
     1.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Wed Jan 11 06:06:12 2023 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Wed Jan 11 09:23:18 2023 +0100
     1.3 @@ -817,7 +817,7 @@
     1.4  
     1.5  (* get the theory explicitly just for the rootpbl;
     1.6     thus use this function _after_ finishing specification *)
     1.7 -fun root_thy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = Know_Store.get_via_last_thy thyID
     1.8 +fun root_thy (Nd (PblObj {spec = (thyID, _, _), ctxt, ...}, _)) = ThyC.get_theory_PIDE ctxt thyID
     1.9    | root_thy _ = raise ERROR "root_thy: uncovered fun def.";
    1.10  
    1.11  (**)