src/Pure/sign.ML

 (* add type constructors *)
 
 fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
     fun type_syntax (b, n, mx) =
-      (Syntax.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
+      (Lexicon.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
     val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
     val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
   in (naming, syn', tsig', consts) end);
 
 

 val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I);
 
 fun type_notation add mode args =
   let
     fun type_syntax (Type (c, args), mx) =
-          SOME (Syntax.mark_type c, Mixfix.make_type (length args), mx)
+          SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx)
       | type_syntax _ = NONE;
   in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
 
 fun notation add mode args thy =
   let
     fun const_syntax (Const (c, _), mx) =
           (case try (Consts.type_scheme (consts_of thy)) c of
-            SOME T => SOME (Syntax.mark_const c, T, mx)
+            SOME T => SOME (Lexicon.mark_const c, T, mx)
           | NONE => NONE)
       | const_syntax _ = NONE;
   in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end;
 
 

       let
         val c = full_name thy b;
         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
           cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
         val T' = Logic.varifyT_global T;
-      in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end;
+      in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end;
     val args = map prep raw_args;
   in
     thy
     |> map_consts (fold (Consts.declare (naming_of thy) o #1) args)
     |> add_syntax_i (map #2 args)