changeset 74302 | 6bc96f31cafd |
parent 69593 | 3dda49e08b9d |
--- a/src/Sequents/modal.ML Sun Sep 12 20:24:14 2021 +0200 +++ b/src/Sequents/modal.ML Sun Sep 12 20:37:15 2021 +0200 @@ -26,7 +26,7 @@ struct (*Returns the list of all formulas in the sequent*) -fun forms_of_seq (Const(\<^const_name>\<open>SeqO'\<close>,_) $ P $ u) = P :: forms_of_seq u +fun forms_of_seq \<^Const_>\<open>SeqO' for P u\<close> = P :: forms_of_seq u | forms_of_seq (H $ u) = forms_of_seq u | forms_of_seq _ = [];