src/HOL/Data_Structures/Leftist_Heap.thy

--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Sun Aug 27 13:02:13 2017 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Sun Aug 27 16:56:25 2017 +0200
@@ -62,6 +62,8 @@
     if a1 \<le> a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge r2 t1))"
 by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
 
+hide_const (open) insert
+
 definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
 "insert x t = merge (Node 1 Leaf x Leaf) t"