adapted to qualified names;

--- a/src/Sequents/ROOT.ML	Mon Oct 20 11:25:39 1997 +0200
+++ b/src/Sequents/ROOT.ML	Mon Oct 20 11:39:29 1997 +0200
@@ -9,6 +9,8 @@
 val banner = "Sequent Calculii";
 writeln banner;
 
+reset global_names;
+
 print_depth 1;  
 
 use_thy "Sequents";

--- a/src/Sequents/prover.ML	Mon Oct 20 11:25:39 1997 +0200
+++ b/src/Sequents/prover.ML	Mon Oct 20 11:39:29 1997 +0200
@@ -29,7 +29,7 @@
 
 
 (*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 _ = [];
 
@@ -160,7 +160,7 @@
 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 _ = [];