src/Pure/type.ML
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