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);