consts: syntax consts only for actual syntax;
authorwenzelm
Thu Sep 28 23:42:56 2006 +0200 (2006-09-28)
changeset 2077700e560b6c112
parent 20776 cc436bcdd5fc
child 20778 f39c733f2a7e
consts: syntax consts only for actual syntax;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Sep 28 23:42:55 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Sep 28 23:42:56 2006 +0200
     1.3 @@ -733,7 +733,6 @@
     1.4    in
     1.5      thy
     1.6      |> map_consts (fold (Consts.declare (naming_of thy) o #1) args)
     1.7 -    |> map_syn (Syntax.extend_consts (map (#1 o #1 o #1) args))
     1.8      |> add_syntax_i (map #2 args)
     1.9    end;
    1.10  
    1.11 @@ -761,7 +760,6 @@
    1.12    in
    1.13      thy
    1.14      |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), true))
    1.15 -    |> map_syn (Syntax.extend_consts [c])
    1.16      |> add_modesyntax_i (mode, inout) [(c', T, mx)]
    1.17    end);
    1.18