src/Pure/Isar/proof_context.ML

 fun read_type_name ctxt strict text =
   let
     val tsig = tsig_of ctxt;
     val (c, pos) = token_content text;
   in
-    if Syntax.is_tid c then
+    if Lexicon.is_tid c then
      (Context_Position.report ctxt pos Markup.tfree;
       TFree (c, default_sort ctxt (c, ~1)))
     else
       let
         val d = Type.intern_type tsig c;

 
 fun prep_vars prep_typ internal =
   fold_map (fn (b, raw_T, mx) => fn ctxt =>
     let
       val x = Name.of_binding b;
-      val _ = Syntax.is_identifier (no_skolem internal x) orelse
+      val _ = Lexicon.is_identifier (no_skolem internal x) orelse
         error ("Illegal variable name: " ^ quote (Binding.str_of b));
 
       fun cond_tvars T =
         if internal then T
         else Type.no_tvars T handle TYPE (msg, _, _) => error msg;

 local
 
 fun const_ast_tr intern ctxt [Ast.Variable c] =
       let
         val Const (c', _) = read_const_proper ctxt false c;
-        val d = if intern then Syntax.mark_const c' else c;
+        val d = if intern then Lexicon.mark_const c' else c;
       in Ast.Constant d end
   | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
 
 val typ = Simple_Syntax.read_typ;
 

 (* notation *)
 
 local
 
 fun type_syntax (Type (c, args), mx) =
-      SOME (Local_Syntax.Type, (Syntax.mark_type c, Mixfix.make_type (length args), mx))
+      SOME (Local_Syntax.Type, (Lexicon.mark_type c, Mixfix.make_type (length args), mx))
   | type_syntax _ = NONE;
 
 fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
   | const_syntax ctxt (Const (c, _), mx) =
       (case try (Consts.type_scheme (consts_of ctxt)) c of
-        SOME T => SOME (Local_Syntax.Const, (Syntax.mark_const c, T, mx))
+        SOME T => SOME (Local_Syntax.Const, (Lexicon.mark_const c, T, mx))
       | NONE => NONE)
   | const_syntax _ _ = NONE;
 
 fun gen_notation syntax add mode args ctxt =
   ctxt |> map_syntax