# HG changeset patch
# User wenzelm
# Date 877340369 -7200
# Node ID 3428c0a884492c04cfc3e0681a2aecaa638b1270
# Parent  eb707467f8c5317869ed64cf5c13f9a6929e7b19
adapted to qualified names;

diff -r eb707467f8c5 -r 3428c0a88449 src/Sequents/ROOT.ML
--- 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";
diff -r eb707467f8c5 -r 3428c0a88449 src/Sequents/prover.ML
--- 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 _ = [];