# 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