--- a/src/Pure/consts.ML Sat Feb 09 12:56:12 2008 +0100
+++ b/src/Pure/consts.ML Sun Feb 10 20:49:42 2008 +0100
@@ -225,7 +225,8 @@
fun declare authentic naming tags (c, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
let
- val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic};
+ val tags' = tags |> Position.default_properties (Position.thread_data ());
+ val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
val decls' = decls |> extend_decls naming (c, ((decl, NONE), serial ()));
in (decls', constraints, rev_abbrevs) end);
@@ -281,7 +282,8 @@
in
consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
let
- val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
+ val tags' = tags |> Position.default_properties (Position.thread_data ());
+ val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
val decls' = decls
|> extend_decls naming (c, ((decl, SOME abbr), serial ()));