diff -r 7858b777569a -r ae9bd644d106 src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Wed Nov 16 15:29:23 2005 +0100
+++ b/src/Sequents/Sequents.thy	Wed Nov 16 17:45:22 2005 +0100
@@ -90,7 +90,7 @@
       (Const("SeqO",dummyT) $ f) $
       (seqcont_tr' s) |
 (*    seqcont_tr' ((a as Abs(_,_,_)) $ s)=
-      seqcont_tr'(betapply(a,s)) | *)
+      seqcont_tr'(Term.betapply(a,s)) | *)
     seqcont_tr' (i $ s) =
       Const("SeqContApp",dummyT) $
       (Const("SeqId",dummyT) $ i) $
@@ -103,7 +103,7 @@
               Const("SeqApp",dummyT) $
               (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
 (*            seq_itr' ((a as Abs(_,_,_)) $ s) =
-              seq_itr'(betapply(a,s)) |    *)
+              seq_itr'(Term.betapply(a,s)) |    *)
             seq_itr' (i $ s) =
               Const("SeqApp",dummyT) $
               (Const("SeqId",dummyT) $ i) $