src/HOL/Data_Structures/Leftist_Heap.thy

--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Jul 04 14:20:47 2019 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Jul 11 18:37:52 2019 +0200
@@ -46,7 +46,6 @@
 
 text \<open>For function \<open>merge\<close>:\<close>
 unbundle pattern_aliases
-declare size_prod_measure[measure_function]
 
 fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
 "merge Leaf t2 = t2" |