# HG changeset patch
# User nipkow
# Date 1577220602 -3600
# Node ID a956b769903e770655024cd9e94d178312e1f640
# Parent  ee9998bb417bbc896e8479c41f01f6b795528f6e
tuned

diff -r ee9998bb417b -r a956b769903e src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy	Mon Dec 23 22:35:54 2019 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Tue Dec 24 21:50:02 2019 +0100
@@ -272,7 +272,7 @@
 subsubsection \<open>Size\<close>
 
 fun diff :: "'a tree \<Rightarrow> nat \<Rightarrow> nat" where
-"diff Leaf 0 = 0" |
+"diff Leaf _ = 0" |
 "diff (Node l x r) n = (if n=0 then 1 else if even n then diff r (n div 2 - 1) else diff l (n div 2))"
 
 fun size_fast :: "'a tree \<Rightarrow> nat" where