src/Pure/Isar/class_declaration.ML
changeset 42375 774df7c59508
parent 42360 da8817d01e7c
child 42402 c7139609b67d
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Sun Apr 17 13:47:22 2011 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Sun Apr 17 19:54:04 2011 +0200
     1.3 @@ -253,7 +253,7 @@
     1.4          val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
     1.5        in
     1.6          thy
     1.7 -        |> Sign.declare_const ((b, ty0), syn)
     1.8 +        |> Sign.declare_const_global ((b, ty0), syn)
     1.9          |> snd
    1.10          |> pair ((Variable.name b, ty), (c, ty'))
    1.11        end;