# HG changeset patch
# User wenzelm
# Date 1159479776 -7200
# Node ID 00e560b6c112257b9c7d6a6d5e71f249641a188b
# Parent  cc436bcdd5fccea5b9732d3617210196344b4a57
consts: syntax consts only for actual syntax;

diff -r cc436bcdd5fc -r 00e560b6c112 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Sep 28 23:42:55 2006 +0200
+++ b/src/Pure/sign.ML	Thu Sep 28 23:42:56 2006 +0200
@@ -733,7 +733,6 @@
   in
     thy
     |> map_consts (fold (Consts.declare (naming_of thy) o #1) args)
-    |> map_syn (Syntax.extend_consts (map (#1 o #1 o #1) args))
     |> add_syntax_i (map #2 args)
   end;
 
@@ -761,7 +760,6 @@
   in
     thy
     |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), true))
-    |> map_syn (Syntax.extend_consts [c])
     |> add_modesyntax_i (mode, inout) [(c', T, mx)]
   end);