src/CTT/Bool.thy

--- a/src/CTT/Bool.thy	Thu Feb 02 09:55:16 2017 -0500
+++ b/src/CTT/Bool.thy	Fri Feb 03 16:36:44 2017 +0100
@@ -19,7 +19,7 @@
   where "false \<equiv> inr(tt)"
 
 definition cond :: "[i,i,i]\<Rightarrow>i"
-  where "cond(a,b,c) \<equiv> when(a, \<lambda>u. b, \<lambda>u. c)"
+  where "cond(a,b,c) \<equiv> when(a, \<lambda>_. b, \<lambda>_. c)"
 
 lemmas bool_defs = Bool_def true_def false_def cond_def