src/Pure/Isar/class_declaration.ML

         val ty0 = Type.strip_sorts ty;
         val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
         val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
       in
         thy
-        |> Sign.declare_const ((b, ty0), syn)
+        |> Sign.declare_const_global ((b, ty0), syn)
         |> snd
         |> pair ((Variable.name b, ty), (c, ty'))
       end;
   in
     thy