src/Sequents/prover.ML

   writeln (cat_lines
    (["Safe rules:"] @ map Display.string_of_thm_without_context safes @
     ["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 _ = [];
 
 (*Tests whether two sequences (left or right sides) could be resolved.
   seqp is a premise (subgoal), seqc is a conclusion of an object-rule.