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