1.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Sun Jan 08 16:19:31 2023 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Sun Jan 08 17:26:00 2023 +0100
     1.3 @@ -815,7 +815,7 @@
     1.4          in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end
     1.5  	  end;
     1.6  
     1.7 -(* get the theory explicitly specified for the rootpbl;
     1.8 +(* get the theory explicitly just for the rootpbl;
     1.9     thus use this function _after_ finishing specification *)
    1.10  fun root_thy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = Know_Store.get_via_last_thy thyID
    1.11    | root_thy _ = raise ERROR "root_thy: uncovered fun def.";