diff -r b1772698bd78 -r 26ff119fb140 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sun Dec 15 22:58:48 2024 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Mon Dec 16 12:55:39 2024 +0100 @@ -373,7 +373,7 @@ val syn = Proof_Context.syntax_of ctxt; val tr = Syntax.parse_translation syn; val normalize = Ast.normalize ctxt {permissive_constraints = false} (Syntax.parse_rules syn); - val (ambig_msgs, asts) = parse_asts ctxt false root input; + val (ambig_msgs, asts) = parse_asts ctxt {raw = false} root input; val results = (map o apsnd o Exn.maps_res) (normalize #> Exn.result (ast_to_term ctxt tr)) asts; in (ambig_msgs, results) end; @@ -493,7 +493,7 @@ val pos = Input.pos_of source; val syms = Input.source_explode source; val ast = - parse_asts ctxt true root (syms, pos) + parse_asts ctxt {raw = true} root (syms, pos) |> uncurry (report_result ctxt pos) |> decode []; val _ = Context_Position.reports_text ctxt (! reports);