src/Pure/axclass.ML

--- a/src/Pure/axclass.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/axclass.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -305,7 +305,7 @@
   in
     thy
     |> Sign.mandatory_path name_inst
-    |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
+    |> Sign.declare_const ((Binding.name c', T'), NoSyn)
     |-> (fn const' as Const (c'', _) =>
       Thm.add_def false true
         (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))