src/HOL/Data_Structures/Binomial_Heap.thy

 text \<open>This function is non-canonical: we omitted a \<open>+1\<close> in the \<open>else\<close>-part,
   to keep the following analysis simpler and more to the point.
 \<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
 "T_insert x ts = T_ins_tree (Node 0 x []) ts + 1"