maintain default position;
authorwenzelm
Sun Feb 10 20:49:42 2008 +0100 (2008-02-10 ago)
changeset 2605088bb26089ef5
parent 26049 8186c03194ed
child 26051 43bcb30a6d97
maintain default position;
src/Pure/consts.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/consts.ML	Sat Feb 09 12:56:12 2008 +0100
     1.2 +++ b/src/Pure/consts.ML	Sun Feb 10 20:49:42 2008 +0100
     1.3 @@ -225,7 +225,8 @@
     1.4  
     1.5  fun declare authentic naming tags (c, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
     1.6    let
     1.7 -    val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic};
     1.8 +    val tags' = tags |> Position.default_properties (Position.thread_data ());
     1.9 +    val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
    1.10      val decls' = decls |> extend_decls naming (c, ((decl, NONE), serial ()));
    1.11    in (decls', constraints, rev_abbrevs) end);
    1.12  
    1.13 @@ -281,7 +282,8 @@
    1.14    in
    1.15      consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
    1.16        let
    1.17 -        val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
    1.18 +        val tags' = tags |> Position.default_properties (Position.thread_data ());
    1.19 +        val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
    1.20          val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
    1.21          val decls' = decls
    1.22            |> extend_decls naming (c, ((decl, SOME abbr), serial ()));
     2.1 --- a/src/Pure/pure_thy.ML	Sat Feb 09 12:56:12 2008 +0100
     2.2 +++ b/src/Pure/pure_thy.ML	Sun Feb 10 20:49:42 2008 +0100
     2.3 @@ -345,7 +345,8 @@
     2.4  
     2.5  fun name_thm pre official name thm = thm
     2.6    |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
     2.7 -  |> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name);
     2.8 +  |> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name)
     2.9 +  |> Thm.map_tags (Position.default_properties (Position.thread_data ()));
    2.10  
    2.11  fun name_thms pre official name xs =
    2.12    map (uncurry (name_thm pre official)) (name_multi name xs);