src/Sequents/modal.ML
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 _ = [];