From 26d70608f82e48de73497ed84fa89b321d7864f3 Mon Sep 17 00:00:00 2001
From: cp526
Date: Fri, 5 Jun 2015 12:48:00 +0100
Subject: slight change of binary_taint for Isabelle

---
 src/lem_interp/interp.lem | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src')

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
-- 
cgit v1.2.3