src/Pure/Syntax/syntax.ML
changeset 81601 26ff119fb140
parent 81596 af21a61dadad
child 81993 f62e7c3ab254
--- a/src/Pure/Syntax/syntax.ML	Sun Dec 15 22:58:48 2024 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Dec 16 12:55:39 2024 +0100
@@ -85,7 +85,7 @@
   val get_consts: syntax -> string -> string list
   val is_const: syntax -> string -> bool
   val is_keyword: syntax -> string -> bool
-  val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
+  val tokenize: syntax -> {raw: bool} -> Symbol_Pos.T list -> Lexicon.token list
   val parse: syntax -> string -> Lexicon.token list -> Parser.tree list
   val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option
   val parse_rules: syntax -> string -> (Ast.ast * Ast.ast) list