adapted to qualified names;
authorwenzelm
Mon Oct 20 11:39:29 1997 +0200 (1997-10-20)
changeset 39483428c0a88449
parent 3947 eb707467f8c5
child 3949 c60ff6d0a6b8
adapted to qualified names;
src/Sequents/ROOT.ML
src/Sequents/prover.ML
     1.1 --- a/src/Sequents/ROOT.ML	Mon Oct 20 11:25:39 1997 +0200
     1.2 +++ b/src/Sequents/ROOT.ML	Mon Oct 20 11:39:29 1997 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  val banner = "Sequent Calculii";
     1.5  writeln banner;
     1.6  
     1.7 +reset global_names;
     1.8 +
     1.9  print_depth 1;  
    1.10  
    1.11  use_thy "Sequents";
     2.1 --- a/src/Sequents/prover.ML	Mon Oct 20 11:25:39 1997 +0200
     2.2 +++ b/src/Sequents/prover.ML	Mon Oct 20 11:39:29 1997 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4  
     2.5  
     2.6  (*Returns the list of all formulas in the sequent*)
     2.7 -fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
     2.8 +fun forms_of_seq (Const("Sequents.SeqO'",_) $ P $ u) = P :: forms_of_seq u
     2.9    | forms_of_seq (H $ u) = forms_of_seq u
    2.10    | forms_of_seq _ = [];
    2.11  
    2.12 @@ -160,7 +160,7 @@
    2.13  in 
    2.14  
    2.15  (*Returns the list of all formulas in the sequent*)
    2.16 -fun forms_of_seq (Const("SeqO",_) $ P $ u) = P :: forms_of_seq u
    2.17 +fun forms_of_seq (Const("Sequents.SeqO",_) $ P $ u) = P :: forms_of_seq u
    2.18    | forms_of_seq (H $ u) = forms_of_seq u
    2.19    | forms_of_seq _ = [];
    2.20