# HG changeset patch
# User haftmann
# Date 1648533737 0
# Node ID f9c758208298f00d60f72ac605abf637989a1243
# Parent  528768bc7bd061427a8e06fa99532e0de6ba5674
tighter check to ensure that patterns remain left-linear, previous implementation was overcautious

diff -r 528768bc7bd0 -r f9c758208298 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Mar 29 06:02:16 2022 +0000
+++ b/src/Tools/Code/code_thingol.ML	Tue Mar 29 06:02:17 2022 +0000
@@ -293,7 +293,7 @@
       restrict_vars_to (build (add_varnames t));
     fun distill' vs_map pat_args v i clauses =
       let
-        val vs = build (fold add_varnames pat_args);
+        val vs = build (fold add_varnames (nth_drop i pat_args));
         fun varnames_disjunctive pat =
           null (inter (op =) vs (build (add_varnames pat)));
       in