# HG changeset patch
# User blanchet
# Date 1604663978 -3600
# Node ID 729d45c7ff3383f4346891283efa5b5573792108
# Parent  1d0ae7e578a0c6859881943509b77d163f91e5c2
undid renaming accident

diff -r 1d0ae7e578a0 -r 729d45c7ff33 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Fri Nov 06 12:48:31 2020 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Fri Nov 06 12:59:38 2020 +0100
@@ -326,7 +326,7 @@
 using assms
 by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
 
-lemma seT_get_min_rest:
+lemma set_get_min_rest:
   assumes "get_min_rest ts = (t', ts')"
   assumes "ts\<noteq>[]"
   shows "set ts = Set.insert t' (set ts')"
@@ -345,7 +345,7 @@
       case (2 t v va)
       then show ?case
         apply (clarsimp split: prod.splits if_splits)
-        apply (drule seT_get_min_rest; fastforce)
+        apply (drule set_get_min_rest; fastforce)
         done
     qed auto
   thus "invar_btree t'" and "invar_bheap ts'" by auto