src/Sequents/prover.ML
changeset 3948 3428c0a88449
parent 3538 ed9de44032e0
child 4440 9ed4098074bc
     1.1 --- a/src/Sequents/prover.ML	Mon Oct 20 11:25:39 1997 +0200
     1.2 +++ b/src/Sequents/prover.ML	Mon Oct 20 11:39:29 1997 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  
     1.6  (*Returns the list of all formulas in the sequent*)
     1.7 -fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
     1.8 +fun forms_of_seq (Const("Sequents.SeqO'",_) $ P $ u) = P :: forms_of_seq u
     1.9    | forms_of_seq (H $ u) = forms_of_seq u
    1.10    | forms_of_seq _ = [];
    1.11  
    1.12 @@ -160,7 +160,7 @@
    1.13  in 
    1.14  
    1.15  (*Returns the list of all formulas in the sequent*)
    1.16 -fun forms_of_seq (Const("SeqO",_) $ P $ u) = P :: forms_of_seq u
    1.17 +fun forms_of_seq (Const("Sequents.SeqO",_) $ P $ u) = P :: forms_of_seq u
    1.18    | forms_of_seq (H $ u) = forms_of_seq u
    1.19    | forms_of_seq _ = [];
    1.20