diff -r afa8cf9e63d8 -r df2862dc23a8 src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Wed Mar 03 00:28:22 2010 +0100
+++ b/src/Sequents/Sequents.thy	Wed Mar 03 00:32:14 2010 +0100
@@ -65,7 +65,7 @@
 
 (* parse translation for sequences *)
 
-fun abs_seq' t = Abs ("s", Type (@{type_syntax seq'}, []), t);
+fun abs_seq' t = Abs ("s", Type (@{type_name seq'}, []), t);
 
 fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
       Const (@{const_syntax SeqO'}, dummyT) $ f