changeset 28941 | 128459bd72d2 |
parent 28863 | 32e83a854e5e |
child 28965 | 1de908189869 |
--- a/src/Pure/sign.ML Mon Dec 01 16:02:57 2008 +0100 +++ b/src/Pure/sign.ML Mon Dec 01 19:41:16 2008 +0100 @@ -535,7 +535,7 @@ fun declare_const tags ((b, T), mx) thy = let - val pos = Name.pos_of b; + val pos = Binding.pos_of b; val tags' = Position.default_properties pos tags; val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy; val _ = Position.report (Markup.const_decl c) pos;