| changeset 35430 | df2862dc23a8 |
| parent 35363 | 09489d8ffece |
| child 38499 | 8f0cd11238a7 |
--- 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