src/HOL/Tools/string_syntax.ML

 
 
 (* nibble *)
 
 val mk_nib =
-  Ast.Constant o Syntax.mark_const o
+  Ast.Constant o Lexicon.mark_const o
     fst o Term.dest_Const o HOLogic.mk_nibble;
 
 fun dest_nib (Ast.Constant s) =
-  (case try Syntax.unmark_const s of
+  (case try Lexicon.unmark_const s of
     NONE => raise Match
   | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
 
 
 (* char *)

 
 fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
   | dest_char _ = raise Match;
 
 fun syntax_string cs =
-  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, Ast.Variable (Syntax.implode_xstr cs)];
+  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
+    Ast.Variable (Lexicon.implode_xstr cs)];
 
 
 fun char_ast_tr [Ast.Variable xstr] =
-      (case Syntax.explode_xstr xstr of
+      (case Lexicon.explode_xstr xstr of
         [c] => mk_char c
       | _ => error ("Single character expected: " ^ xstr))
   | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
 
 fun char_ast_tr' [c1, c2] =

 fun mk_string [] = Ast.Constant @{const_syntax Nil}
   | mk_string (c :: cs) =
       Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
 
 fun string_ast_tr [Ast.Variable xstr] =
-      (case Syntax.explode_xstr xstr of
+      (case Lexicon.explode_xstr xstr of
         [] =>
           Ast.Appl
             [Ast.Constant @{syntax_const "_constrain"},
               Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
       | cs => mk_string cs)