src/Pure/Isar/class_declaration.ML
changeset 42375 774df7c59508
parent 42360 da8817d01e7c
child 42402 c7139609b67d
--- a/src/Pure/Isar/class_declaration.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -253,7 +253,7 @@
         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;