# HG changeset patch
# User nipkow
# Date 1609842275 -3600
# Node ID 2138a4a9031ab8775086e7313eddc6724a3dd08a
# Parent  c03a148110cc5505c2c5b58a168c75b6c7832ace
tuned

diff -r c03a148110cc -r 2138a4a9031a src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Tue Jan 05 03:35:46 2021 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Tue Jan 05 11:24:35 2021 +0100
@@ -483,9 +483,9 @@
 \<close>
 fun T_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where
   "T_ins_tree t [] = 1"
-| "T_ins_tree t\<^sub>1 (t\<^sub>2 # rest) = (
+| "T_ins_tree t\<^sub>1 (t\<^sub>2 # ts) = (
     (if rank t\<^sub>1 < rank t\<^sub>2 then 1
-     else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) rest)
+     else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) ts)
   )"
 
 definition T_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where