diff --git a/bil.ott b/bil.ott
index 335c29f..85e08f9 100644
--- a/bil.ott
+++ b/bil.ott
@@ -459,7 +459,7 @@ defns program :: '' ::=
  defn delta , w , var ~> delta' , w' , var' :: :: step :: '' by
 
  delta,w,var |-> {addr=w1; size=w2; code=bil}
- delta, w1.+w2 |- bil ~> delta',w3,{}
+ delta, w1.+w2 |- bil ~> delta',w3
  ---------------------------------------------------------- :: step
  delta,w,var  ~> delta',w3,var
 
@@ -790,23 +790,23 @@ defns reduce_stmt :: '' ::=
 
 
  delta |- e ~>* true
- delta,word |- seq ~> delta',word',{}
+ delta,word |- seq ~> delta',word'
  ------------------------------------- :: ifthen_true
  delta,word |- if (e) seq ~> delta', word'
 
  delta |- e ~>* true
- delta,word |- seq ~> delta',word',{}
+ delta,word |- seq ~> delta',word'
  ------------------------------------- :: if_true
  delta,word |- if (e) seq else seq1 ~> delta', word'
 
  delta |- e ~>* false
- delta,word |- seq ~> delta',word',{}
+ delta,word |- seq ~> delta',word'
  ------------------------------------- :: if_false
  delta,word |- if (e) seq1 else seq ~> delta', word'
 
 
  delta1 |- e ~>* true
- delta1,word1 |- seq ~> delta2,word2,{}
+ delta1,word1 |- seq ~> delta2,word2
  delta2,word2 |- while (e) seq ~> delta3,word3
  --------------------------------------------- :: while
  delta1,word1 |- while (e) seq ~> delta3,word3
@@ -819,21 +819,18 @@ defns reduce_stmt :: '' ::=
 
  defn delta , word |- seq ~> delta' , word' , seq' :: :: seq :: '' by
 
- delta,word |- s1 ~> delta',word'
- ------------------------------------------------------------- :: seq_rec
- delta,word |- {s1; s2; ..; sn} ~> delta', word', {s2; ..; sn}
-
- delta,word |- s1 ~> delta',word'
- ------------------------------------------------------------- :: seq_last
- delta,word |- {s1; s2} ~> delta', word', {s2}
+ delta1,word1 |- s1 ~> delta2,word2
+ delta2,word2 |- {s2; ..; sn} ~> delta3, word3
+------------------------------------------------------------- :: seq_rec
+ delta1,word1 |- {s1; s2; ..; sn} ~> delta3, word3
 
  delta,word |- s1 ~> delta',word'
  ------------------------------------------------------------- :: seq_one
- delta,word |- {s1} ~> delta', word', {}
+ delta,word |- {s1} ~> delta', word'
 
 
  ------------------------------------------------------------- :: seq_nil
- delta,word |- {} ~> delta, word, {}
+ delta,word |- {} ~> delta, word
  
 defns multistep_exp :: '' ::=