# HG changeset patch
# User wenzelm
# Date 1159479779 -7200
# Node ID f39c733f2a7e0d2f197dcfe4d316af73314e10ba
# Parent  00e560b6c112257b9c7d6a6d5e71f249641a188b
Sign.add_consts_authentic;

diff -r 00e560b6c112 -r f39c733f2a7e src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Sep 28 23:42:56 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Sep 28 23:42:59 2006 +0200
@@ -197,7 +197,7 @@
     (case locale_of ctxt of
       NONE => theory (Sign.add_consts_authentic (map (fn ((c, T), mx) => (c, T, mx)) decls))
     | SOME (loc, _) =>
-        theory (Sign.add_consts_i (map (fn ((c, T), _) => (c, Ps ---> T, NoSyn)) decls)) #>
+        theory (Sign.add_consts_authentic (map (fn ((c, T), _) => (c, Ps ---> T, NoSyn)) decls)) #>
         abbrevs Syntax.default_mode abbrs)
     |> pair (map #2 abbrs)
   end;