src/Pure/pure_thy.ML

--- a/src/Pure/pure_thy.ML	Sun Sep 30 11:55:14 2007 +0200
+++ b/src/Pure/pure_thy.ML	Sun Sep 30 16:20:31 2007 +0200
@@ -499,7 +499,7 @@
     val def = Logic.mk_equals (list_comb (Const (c, ty), ts), t);
   in
     thy
-    |> Sign.add_consts_authentic [(raw_c, ty, syn)]
+    |> Sign.add_consts_authentic [] [(raw_c, ty, syn)]
     |> add_defs_i false [((name, def), atts)]
     |-> (fn [thm] => pair (c, thm))
   end;