# HG changeset patch
# User wenzelm
# Date 1727341301 -7200
# Node ID 6b8e746aed55f5b2276f5d9e1f5f927bb2b5767e
# Parent  4547a3674d10ddc84bf00de1f02f59018596be4e
unused (see 584828fa7a97);

diff -r 4547a3674d10 -r 6b8e746aed55 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Thu Sep 26 10:51:36 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Thu Sep 26 11:01:41 2024 +0200
@@ -552,9 +552,6 @@
 
 fun movedot_nonterm tt (info, Nonterminal _ :: sa, ts) : state = (info, sa, tt @ ts);
 
-fun movedot_lambda p ((info, sa, ts): state) =
-  map_filter (fn (t, k) => if p <= k then SOME (info, sa, t @ ts) else NONE);
-
 
 (*trigger value for warnings*)
 val branching_level = Config.declare_int ("syntax_branching_level", \<^here>) (K 600);