src/Sequents/prover.ML

 fun (Pack(safes,unsafes)) add_unsafes ths = 
     Pack(safes, sort less (ths@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("Sequents.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.

 struct
 local open Modal_Rule
 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("Sequents.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.