don't use Loc_None in typed_parse_in_context

HOL-Theorem-Prover · Nov 17, 2024 · e568888 · e568888
1 parent 9666317
commit e568888
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/parse/Parse.sml b/src/parse/Parse.sml
@@ -483,7 +483,9 @@ fun grammar_typed_parse_in_context gs ty ctxt q =
 
 fun typed_parse_in_context ty ctxt q =
   let
-    fun mkA q = Absyn.TYPED(locn.Loc_None, Absyn q, Pretype.fromType ty)
+    fun mkA q = let
+      val a = Absyn q
+      in Absyn.TYPED(Absyn.locn_of_absyn a, a, Pretype.fromType ty) end
   in
     case seq.cases (TermParse.prim_ctxt_termS mkA (term_grammar()) ctxt q) of
         SOME (tm, _) => tm