# HG changeset patch
# User wenzelm
# Date 1695653711 -7200
# Node ID 5c40df5f0ce9338e94423f35f5d12e11e884935f
# Parent  c7b2697094ac8de45320a1a3b416c0b65056814b
unused;

diff -r c7b2697094ac -r 5c40df5f0ce9 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Mon Sep 25 16:17:43 2023 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Mon Sep 25 16:55:11 2023 +0200
@@ -344,8 +344,6 @@
 
 local
 
-val tokenize = ML_Lex.tokenize_no_range;
-val tokenize_range = ML_Lex.tokenize_range o Input.range_of;
 val tokenize_text = map Antiquote.Text o ML_Lex.tokenize_no_range;
 
 val bg_expr = tokenize_text "(fn () =>";