equal
deleted
inserted
replaced
815 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end |
815 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end |
816 end; |
816 end; |
817 |
817 |
818 (* get the theory explicitly just for the rootpbl; |
818 (* get the theory explicitly just for the rootpbl; |
819 thus use this function _after_ finishing specification *) |
819 thus use this function _after_ finishing specification *) |
820 fun root_thy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = Know_Store.get_via_last_thy thyID |
820 fun root_thy (Nd (PblObj {spec = (thyID, _, _), ctxt, ...}, _)) = ThyC.get_theory_PIDE ctxt thyID |
821 | root_thy _ = raise ERROR "root_thy: uncovered fun def."; |
821 | root_thy _ = raise ERROR "root_thy: uncovered fun def."; |
822 |
822 |
823 (**) |
823 (**) |
824 end; |
824 end; |
825 (**) |
825 (**) |