| changeset 35363 | 09489d8ffece |
| parent 35113 | 1a0c129bb2e0 |
| child 35430 | df2862dc23a8 |
--- a/src/Sequents/Sequents.thy Thu Feb 25 22:15:27 2010 +0100 +++ b/src/Sequents/Sequents.thy Thu Feb 25 22:17:33 2010 +0100 @@ -65,7 +65,7 @@ (* parse translation for sequences *) -fun abs_seq' t = Abs ("s", Type ("seq'", []), t); (* FIXME @{type_syntax} *) +fun abs_seq' t = Abs ("s", Type (@{type_syntax seq'}, []), t); fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) = Const (@{const_syntax SeqO'}, dummyT) $ f