Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Sequents/prover.ML
changeset 3948 3428c0a88449
parent 3538 ed9de44032e0
child 4440 9ed4098074bc 
--- 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 _ = [];
isabelle