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 (**)