changeset 38500 | d5477ee35820 |
parent 32960 | 69916a850301 |
child 41449 | 7339f0e7c513 |
--- a/src/Sequents/modal.ML Tue Aug 17 19:36:38 2010 +0200 +++ b/src/Sequents/modal.ML Tue Aug 17 19:36:39 2010 +0200 @@ -29,7 +29,7 @@ in (*Returns the list of all formulas in the sequent*) -fun forms_of_seq (Const("SeqO",_) $ P $ u) = P :: forms_of_seq u +fun forms_of_seq (Const(@{const_name SeqO'},_) $ P $ u) = P :: forms_of_seq u | forms_of_seq (H $ u) = forms_of_seq u | forms_of_seq _ = [];