src/Pure/sign.ML
changeset 42290 b1f544c84040
parent 42288 2074b31650e6
child 42294 0f4372a2d2e4
     1.1 --- a/src/Pure/sign.ML	Fri Apr 08 15:48:14 2011 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Apr 08 16:34:14 2011 +0200
     1.3 @@ -334,7 +334,7 @@
     1.4  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
     1.5    let
     1.6      fun type_syntax (b, n, mx) =
     1.7 -      (Syntax.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
     1.8 +      (Lexicon.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
     1.9      val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
    1.10      val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
    1.11    in (naming, syn', tsig', consts) end);
    1.12 @@ -373,7 +373,7 @@
    1.13  fun type_notation add mode args =
    1.14    let
    1.15      fun type_syntax (Type (c, args), mx) =
    1.16 -          SOME (Syntax.mark_type c, Mixfix.make_type (length args), mx)
    1.17 +          SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx)
    1.18        | type_syntax _ = NONE;
    1.19    in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
    1.20  
    1.21 @@ -381,7 +381,7 @@
    1.22    let
    1.23      fun const_syntax (Const (c, _), mx) =
    1.24            (case try (Consts.type_scheme (consts_of thy)) c of
    1.25 -            SOME T => SOME (Syntax.mark_const c, T, mx)
    1.26 +            SOME T => SOME (Lexicon.mark_const c, T, mx)
    1.27            | NONE => NONE)
    1.28        | const_syntax _ = NONE;
    1.29    in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end;
    1.30 @@ -401,7 +401,7 @@
    1.31          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.32            cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
    1.33          val T' = Logic.varifyT_global T;
    1.34 -      in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end;
    1.35 +      in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end;
    1.36      val args = map prep raw_args;
    1.37    in
    1.38      thy