src/Pure/Syntax/syntax_phases.ML
changeset 81601 26ff119fb140
parent 81599 ca6b2e49424b
child 81743 fac2045e61d5
--- 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);