tighter check to ensure that patterns remain left-linear, previous implementation was overcautious
--- 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