| changeset 38514 | bd9c4e8281ec |
| parent 37145 | 01aa36932739 |
| child 39288 | f1ae2493d93f |
--- a/src/ZF/ind_syntax.ML Wed Aug 18 12:08:21 2010 +0200 +++ b/src/ZF/ind_syntax.ML Wed Aug 18 12:19:27 2010 +0200 @@ -18,7 +18,7 @@ (** Abstract syntax definitions for ZF **) -val iT = Type("i",[]); +val iT = Type(@{type_name i}, []); (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) fun mk_all_imp (A,P) =