src/HOL/Data_Structures/Binomial_Heap.thy

--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Tue May 08 10:14:36 2018 +0200
@@ -133,7 +133,7 @@
 lemma invar_bheap_Cons[simp]:
   "invar_bheap (t#ts)
   \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
-by (auto simp: sorted_wrt_Cons invar_bheap_def)
+by (auto simp: invar_bheap_def)
 
 lemma invar_btree_ins_tree:
   assumes "invar_btree t"