diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Nov 26 16:37:56 1998 +0100
@@ -104,16 +104,6 @@
              | x##xs => (case t2 of 
                           nil => UU 
                         | y##ys => <x,y>##(h`xs`ys))))"
- 
-(*
-nproj_def 
- "nproj == (%n tr.HD`(iterate n TL tr))"   
-
-
-sproj_def 
- "sproj == (%n tr.iterate n TL tr)"   
-*)
-
 
 Partial_def
   "Partial x  == (seq_finite x) & ~(Finite x)"