diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp.lem | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 2ac078ba..de4938f8 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -449,7 +449,8 @@ let rec detaint value = | v -> v end -let rec binary_taint thunk vall valr = +(* the inner lambda is to make Isabelle happier about overlapping patterns *) +let rec binary_taint thunk = fun vall valr -> match (vall,valr) with | (V_track vl rl,V_track vr rr) -> taint (binary_taint thunk vl vr) (rl++rr) | (V_track vl rl,vr) -> taint (binary_taint thunk vl vr) rl |