changeset 38500 | d5477ee35820 |
parent 33049 | c38f02fdf35d |
child 55228 | 901a6696cdd8 |
--- a/src/Sequents/prover.ML Tue Aug 17 19:36:38 2010 +0200 +++ b/src/Sequents/prover.ML Tue Aug 17 19:36:39 2010 +0200 @@ -55,7 +55,7 @@ ["Unsafe rules:"] @ map Display.string_of_thm_without_context unsafes)); (*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 _ = [];