changeset 33097 | 9d501e11084a |
parent 33096 | db3c18fd9708 |
child 33173 | b8ca12f6681a |
--- a/src/Pure/type.ML Sat Oct 24 20:54:08 2009 +0200 +++ b/src/Pure/type.ML Sat Oct 24 21:30:33 2009 +0200 @@ -556,10 +556,7 @@ local fun new_decl naming tags (c, decl) types = - let - val tags' = tags |> Position.default_properties (Position.thread_data ()); - val (_, types') = Name_Space.define true naming (c, (decl, tags')) types; - in types' end; + #2 (Name_Space.define true naming (c, (decl, tags)) types); fun map_types f = map_tsig (fn (classes, default, types) => let