src/Pure/sign.ML
changeset 33097 9d501e11084a
parent 33095 bbd52d2f8696
child 33157 56f836b9414f
     1.1 --- a/src/Pure/sign.ML	Sat Oct 24 20:54:08 2009 +0200
     1.2 +++ b/src/Pure/sign.ML	Sat Oct 24 21:30:33 2009 +0200
     1.3 @@ -526,8 +526,7 @@
     1.4  fun declare_const tags ((b, T), mx) thy =
     1.5    let
     1.6      val pos = Binding.pos_of b;
     1.7 -    val tags' = Position.default_properties pos tags;
     1.8 -    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy;
     1.9 +    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags [(b, T, mx)] thy;
    1.10      val _ = Position.report (Markup.const_decl c) pos;
    1.11    in (const, thy') end;
    1.12