3 files changed, 1 insertions, 10 deletions
diff --git a/language/l2.lem b/language/l2.lem
index 90974dfc..d39c7110 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -283,10 +283,6 @@ type def =  (* Top-level definition *)
  | DEF_scattered_end of id (* scattered definition end *)
 
 
-type ts = 
- | Ts_lst of list t
-
-
 type defs =  (* Definition sequence *)
  | Defs of list def
 
diff --git a/language/l2.ml b/language/l2.ml
index feb1ca32..bf87b48b 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -457,11 +457,6 @@ type
 
 
 type 
-ts = 
-   Ts_lst of (t) list
-
-
-type 
 'a defs =  (* Definition sequence *)
    Defs of ('a def) list
 
diff --git a/language/l2.ott b/language/l2.ott
index f129d9c4..2e37a490 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -1215,7 +1215,7 @@ terminals :: '' ::=
   | consistent_decrease                 :: :: cd
     {{ tex \ottkw{consistent\_decrease}~ }}
 
-ts :: ts_ ::=
+ts :: ts_ ::=                                     {{ phantom }}
   | t1 , .. , tn :: :: lst 
 
 formula :: formula_ ::=