# HG changeset patch
# User nipkow
# Date 1562863072 -7200
# Node ID 6d96ee03b62e823293ea20fc72f7950ffa08a672
# Parent  421727c19b23cf650622899522fda594a895bf8b
tuned

diff -r 421727c19b23 -r 6d96ee03b62e 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" |