diff --git a/thys/Amortized_Complexity/Pairing_Heap_Tree_Analysis.thy b/thys/Amortized_Complexity/Pairing_Heap_Tree_Analysis.thy
--- a/thys/Amortized_Complexity/Pairing_Heap_Tree_Analysis.thy
+++ b/thys/Amortized_Complexity/Pairing_Heap_Tree_Analysis.thy
@@ -1,268 +1,267 @@
 (* Author: Hauke Brinkop and Tobias Nipkow *)
 
 section \<open>Pairing Heaps\<close>
 
 subsection \<open>Binary Tree Representation\<close>
 
 theory Pairing_Heap_Tree_Analysis
 imports  
   Pairing_Heap.Pairing_Heap_Tree
   Amortized_Framework
   Priority_Queue_ops_merge
   Lemmas_log
 begin
 
 text
 \<open>Verification of logarithmic bounds on the amortized complexity of
 pairing heaps \cite{FredmanSST86,Brinkop}.\<close>
 
 fun len :: "'a tree \<Rightarrow> nat" where 
   "len Leaf = 0"
 | "len (Node _ _ r) = 1 + len r"
 
 fun \<Phi> :: "'a tree \<Rightarrow> real" where
   "\<Phi> Leaf = 0"
 | "\<Phi> (Node l x r) = log 2 (size (Node l x r)) + \<Phi> l + \<Phi> r"
 
 lemma link_size[simp]: "size (link hp) = size hp" 
   by (cases hp rule: link.cases) simp_all
 
 lemma size_pass\<^sub>1: "size (pass\<^sub>1 hp) = size hp" 
   by (induct hp rule: pass\<^sub>1.induct) simp_all
 
 lemma size_pass\<^sub>2: "size (pass\<^sub>2 hp) = size hp" 
   by (induct hp rule: pass\<^sub>2.induct) simp_all
 
 lemma size_merge: 
   "is_root h1 \<Longrightarrow> is_root h2 \<Longrightarrow> size (merge h1 h2) = size h1 + size h2"
   by (simp split: tree.splits)
 
 lemma \<Delta>\<Phi>_insert: "is_root hp \<Longrightarrow> \<Phi> (insert x hp) - \<Phi> hp \<le> log 2  (size hp + 1)"
   by (simp split: tree.splits)
 
 lemma \<Delta>\<Phi>_merge:
   assumes "h1 = Node hs1 x1 Leaf" "h2 = Node hs2 x2 Leaf" 
   shows "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (size h1 + size h2) + 1" 
 proof -
   let ?hs = "Node hs1 x1 (Node hs2 x2 Leaf)"
   have "\<Phi> (merge h1 h2) = \<Phi> (link ?hs)" using assms by simp
   also have "\<dots> = \<Phi> hs1 + \<Phi> hs2 + log 2 (size hs1 + size hs2 + 1) + log 2 (size hs1 + size hs2 + 2)"
     by (simp add: algebra_simps)
   also have "\<dots> = \<Phi> hs1 + \<Phi> hs2 + log 2 (size hs1 + size hs2 + 1) + log 2 (size h1 + size h2)"
      using assms by simp
   finally have "\<Phi> (merge h1 h2) = \<dots>" .
   have "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 =
    log 2 (size hs1 + size hs2 + 1) + log 2 (size h1 + size h2)
    - log 2 (size hs1 + 1) - log 2 (size hs2 + 1)"
      using assms by (simp add: algebra_simps)
   also have "\<dots> \<le> log 2 (size h1 + size h2) + 1"
     using ld_le_2ld[of "size hs1" "size hs2"] assms by (simp add: algebra_simps)
   finally show ?thesis .
 qed
 
 fun ub_pass\<^sub>1 :: "'a tree \<Rightarrow> real" where
-  "ub_pass\<^sub>1 Leaf = 0"
-| "ub_pass\<^sub>1 (Node _ _ Leaf) = 0"
+  "ub_pass\<^sub>1 (Node _ _ Leaf) = 0"
 | "ub_pass\<^sub>1 (Node hs1 _ (Node hs2 _ Leaf)) = 2*log 2 (size hs1 + size hs2 + 2)" 
 | "ub_pass\<^sub>1 (Node hs1 _ (Node hs2 _ hs)) = 2*log 2 (size hs1 + size hs2 + size hs + 2) 
     - 2*log 2 (size hs) - 2 + ub_pass\<^sub>1 hs"
 
-lemma \<Delta>\<Phi>_pass1_ub_pass1: "\<Phi> (pass\<^sub>1 hs) - \<Phi> hs  \<le> ub_pass\<^sub>1 hs"
+lemma \<Delta>\<Phi>_pass1_ub_pass1: "hs \<noteq> Leaf \<Longrightarrow> \<Phi> (pass\<^sub>1 hs) - \<Phi> hs  \<le> ub_pass\<^sub>1 hs"
 proof (induction hs rule: ub_pass\<^sub>1.induct)
-  case (3 lx x ly y)
+  case (2 lx x ly y)
   have "log 2  (size lx + size ly + 1) - log 2  (size ly + 1) 
     \<le> log 2 (size lx + size ly + 1)" by simp
   also have "\<dots> \<le> log 2 (size lx + size ly + 2)" by simp
   also have "\<dots> \<le> 2*\<dots>" by simp
   finally show ?case by (simp add: algebra_simps)
 next
-  case (4 lx x ly y lz z rz)
+  case (3 lx x ly y lz z rz)
   let ?ry = "Node lz z rz"
   let ?rx = "Node ly y ?ry"
   let ?h = "Node lx x ?rx"
   let ?t ="log 2 (size lx + size ly + 1) - log 2 (size ly + size ?ry + 1)"
   have "\<Phi> (pass\<^sub>1 ?h) - \<Phi> ?h \<le> ?t + ub_pass\<^sub>1 ?ry" 
-    using "4.IH" by (simp add: size_pass\<^sub>1 algebra_simps)
+    using "3.IH" by (simp add: size_pass\<^sub>1 algebra_simps)
   moreover have "log 2 (size lx + size ly + 1) + 2 * log 2 (size ?ry) + 2
     \<le> 2 * log 2 (size ?h) + log 2 (size ly + size ?ry + 1)" (is "?l \<le> ?r")
   proof -
     have "?l \<le> 2 * log 2 (size lx + size ly + size ?ry + 1) + log 2 (size ?ry)"
       using ld_sum_inequality [of "size lx + size ly + 1" "size ?ry"] by simp
     also have "\<dots> \<le> 2 * log 2 (size lx + size ly + size ?ry + 2) + log 2 (size ?ry)"
       by simp
     also have "\<dots> \<le> ?r" by simp
     finally show ?thesis .
   qed
   ultimately show ?case by simp
 qed simp_all
 
 lemma \<Delta>\<Phi>_pass1: assumes "hs \<noteq> Leaf"
   shows "\<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le> 2*log 2 (size hs) - len hs + 2"
 proof -
   from assms have "ub_pass\<^sub>1 hs \<le> 2*log 2 (size hs) - len hs + 2" 
     by (induct hs rule: ub_pass\<^sub>1.induct) (simp_all add: algebra_simps)
-  thus ?thesis using \<Delta>\<Phi>_pass1_ub_pass1 [of "hs"] order_trans by blast
+  thus ?thesis using \<Delta>\<Phi>_pass1_ub_pass1 [OF assms] order_trans by blast
 qed
 
 lemma \<Delta>\<Phi>_pass2: "hs \<noteq> Leaf \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi> hs \<le> log 2 (size hs)"
 proof (induction hs)
   case (Node lx x rx)
   thus ?case 
   proof (cases rx)
     case 1: (Node ly y ry)
     let ?h = "Node lx x rx"
     obtain la a where 2: "pass\<^sub>2 rx = Node la a Leaf" 
       using pass\<^sub>2_struct 1 by force
     hence 3: "size rx = size \<dots>" using size_pass\<^sub>2 by metis
     have link: "\<Phi>(link(Node lx x (pass\<^sub>2 rx))) - \<Phi> lx - \<Phi> (pass\<^sub>2 rx) =
           log 2 (size lx + size rx + 1) + log 2 (size lx + size rx) - log 2 (size rx)"
       using 2 3 by (simp add: algebra_simps) 
     have "\<Phi> (pass\<^sub>2 ?h) - \<Phi> ?h =
         \<Phi> (link (Node lx x (pass\<^sub>2 rx))) - \<Phi> lx - \<Phi> rx - log 2 (size lx + size rx + 1)"
       by (simp)
     also have "\<dots> = \<Phi> (pass\<^sub>2 rx) - \<Phi> rx + log 2 (size lx + size rx) - log 2 (size rx)"
       using link by linarith
     also have "\<dots> \<le> log 2 (size lx + size rx)"
       using Node.IH 1 by simp
     also have "\<dots> \<le> log 2 (size ?h)" using 1 by simp
     finally show ?thesis .
   qed simp
 qed simp
 (*
 lemma \<Delta>\<Phi>_mergepairs: assumes "hs \<noteq> Leaf"
   shows "\<Phi> (merge_pairs hs) - \<Phi> hs \<le> 3 * log 2 (size hs) - len hs + 2"
 proof -
   have "pass\<^sub>1 hs \<noteq> Leaf" by (metis assms eq_size_0 size_pass\<^sub>1)
   with assms \<Delta>\<Phi>_pass1[of hs] \<Delta>\<Phi>_pass2[of "pass\<^sub>1 hs"]
   show ?thesis by (auto simp add: size_pass\<^sub>1 pass12_merge_pairs)
 qed
 *)
 lemma \<Delta>\<Phi>_del_min: assumes "hs \<noteq> Leaf"
 shows "\<Phi> (del_min (Node hs x Leaf)) - \<Phi> (Node hs x Leaf) 
   \<le> 3*log 2 (size hs) - len hs + 2"
 proof -
   let ?h = "Node hs x Leaf"
   let ?\<Delta>\<Phi>\<^sub>1 = "\<Phi> hs - \<Phi> ?h" 
   let ?\<Delta>\<Phi>\<^sub>2 = "\<Phi>(pass\<^sub>2(pass\<^sub>1 hs)) - \<Phi> hs"
   let ?\<Delta>\<Phi> = "\<Phi> (del_min ?h) - \<Phi> ?h"
   have "\<Phi>(pass\<^sub>2(pass\<^sub>1 hs)) - \<Phi> (pass\<^sub>1 hs) \<le> log 2  (size hs)" 
     using \<Delta>\<Phi>_pass2 [of "pass\<^sub>1 hs"] assms by(metis eq_size_0 size_pass\<^sub>1)
   moreover have "\<Phi> (pass\<^sub>1 hs) - \<Phi> hs \<le>  2*\<dots> - len hs + 2" 
     by(rule \<Delta>\<Phi>_pass1[OF assms])
   moreover have "?\<Delta>\<Phi> \<le> ?\<Delta>\<Phi>\<^sub>2" by simp
   ultimately show ?thesis using assms by linarith
 qed
 
 lemma is_root_merge:
   "is_root h1 \<Longrightarrow> is_root h2 \<Longrightarrow> is_root (merge h1 h2)"
 by (simp split: tree.splits)
 
 lemma is_root_insert: "is_root h \<Longrightarrow> is_root (insert x h)"
 by (simp split: tree.splits)
 
 lemma is_root_del_min:
   assumes "is_root h" shows "is_root (del_min h)"
 proof (cases h)
   case [simp]: (Node lx x rx)
   have "rx = Leaf" using assms by simp
   thus ?thesis 
   proof (cases lx)
     case (Node ly y ry)
     then obtain la a ra where "pass\<^sub>1 lx = Node a la ra" 
       using pass\<^sub>1_struct by blast
     moreover obtain lb b where "pass\<^sub>2 \<dots> = Node b lb Leaf"
       using pass\<^sub>2_struct by blast
     ultimately show ?thesis using assms by simp
   qed simp
 qed simp
 
 lemma pass\<^sub>1_len: "len (pass\<^sub>1 h) \<le> len h"
 by (induct h rule: pass\<^sub>1.induct) simp_all
 
 fun exec :: "'a :: linorder op \<Rightarrow> 'a tree list \<Rightarrow> 'a tree" where
 "exec Empty [] = Leaf" | 
 "exec Del_min [h] = del_min h" |
 "exec (Insert x) [h] = insert x h" |
 "exec Merge [h1,h2] = merge h1 h2"
 
 fun T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 :: "'a tree \<Rightarrow> nat" where
   "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 Leaf = 1"
 | "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (Node _ _ Leaf) = 1"
 | "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (Node _ _ (Node _ _ ry)) = T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 ry + 1"
 
 fun T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 :: "'a tree \<Rightarrow> nat" where
   "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 Leaf = 1"
 | "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (Node _ _ rx) = T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 rx + 1"
 
 fun cost :: "'a :: linorder op \<Rightarrow> 'a tree list \<Rightarrow> nat" where
   "cost Empty [] = 1"
 | "cost Del_min [Leaf] = 1"
 | "cost Del_min [Node lx _  _] = T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 lx) + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 lx"
 | "cost (Insert a) _ = 1"
 | "cost Merge _ = 1"
 
 fun U :: "'a :: linorder op \<Rightarrow> 'a tree list \<Rightarrow> real" where
   "U Empty [] = 1"
 | "U (Insert a) [h] = log 2 (size h + 1) + 1"
 | "U Del_min [h] = 3*log 2 (size h + 1) + 4"
 | "U Merge [h1,h2] = log 2 (size h1 + size h2 + 1) + 2"
 
 interpretation Amortized
 where arity = arity and exec = exec and cost = cost and inv = is_root 
 and \<Phi> = \<Phi> and U = U
 proof (standard, goal_cases)
   case (1 _ f) thus ?case using is_root_insert is_root_del_min is_root_merge
     by (cases f) (auto simp: numeral_eq_Suc)
 next
   case (2 s) show ?case by (induct s) simp_all
 next
   case (3 ss f) show ?case 
   proof (cases f)
     case Empty with 3 show ?thesis by(auto)
   next
     case (Insert x)
     then obtain h where "ss = [h]" "is_root h" using 3 by auto
     thus ?thesis using Insert \<Delta>\<Phi>_insert 3 by auto
   next
     case [simp]: (Del_min)
     then obtain h where [simp]: "ss = [h]" using 3 by auto
     show ?thesis
     proof (cases h)
       case [simp]: (Node lx x rx)
       have "T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (pass\<^sub>1 lx) + T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 lx \<le> len lx + 2"
         by (induct lx rule: pass\<^sub>1.induct) simp_all
       hence "cost f ss \<le> \<dots>" by simp 
       moreover have "\<Phi> (del_min h) - \<Phi> h \<le> 3*log 2 (size h + 1) - len lx + 2"
       proof (cases lx)
         case [simp]: (Node ly y ry) 
         have "\<Phi> (del_min h) - \<Phi> h \<le> 3*log 2 (size lx) - len lx + 2"
           using  \<Delta>\<Phi>_del_min[of "lx" "x"] 3 by simp
         also have "\<dots> \<le> 3*log 2 (size h + 1) - len lx + 2" by fastforce
         finally show ?thesis by blast
       qed (insert 3, simp)
       ultimately show ?thesis by auto
     qed simp
   next
     case [simp]: Merge
     then obtain h1 h2 where [simp]: "ss = [h1,h2]" and 1: "is_root h1" "is_root h2"
       using 3 by (auto simp: numeral_eq_Suc)
     show ?thesis
     proof (cases h1)
       case Leaf thus ?thesis by (cases h2) auto
     next
       case h1: Node
       show ?thesis
       proof (cases h2)
         case Leaf thus ?thesis using h1 by simp
       next
         case h2: Node
         have "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1"
           apply(rule \<Delta>\<Phi>_merge) using h1 h2 1 by auto
         also have "\<dots> \<le> log 2 (size h1 + size h2 + 1) + 1" by (simp add: h1)
         finally show ?thesis by(simp add: algebra_simps)
       qed
     qed
   qed
 qed
 
 end
diff --git a/thys/CakeML_Codegen/Test/Test_Embed_Data2.thy b/thys/CakeML_Codegen/Test/Test_Embed_Data2.thy
--- a/thys/CakeML_Codegen/Test/Test_Embed_Data2.thy
+++ b/thys/CakeML_Codegen/Test/Test_Embed_Data2.thy
@@ -1,44 +1,42 @@
 theory Test_Embed_Data2
 imports
   Lazy_Case.Lazy_Case
   "../Preproc/Embed"
   "../Preproc/Eval_Instances"
   "Pairing_Heap.Pairing_Heap_Tree"
 begin
 
 declare List.Ball_set[code_unfold]
 
 lemma [code_unfold]: "(\<forall>x \<in> set_tree l. P x) \<longleftrightarrow> list_all P (inorder l)"
   by (induction l) auto
 
 declassify valid:
   Pairing_Heap_Tree.link
   Pairing_Heap_Tree.pass\<^sub>1
   Pairing_Heap_Tree.pass\<^sub>2
-  Pairing_Heap_Tree.merge_pairs
   Pairing_Heap_Tree.is_root
   Pairing_Heap_Tree.pheap
 
 thm valid
 
 derive evaluate
   Tree.tree
   Orderings_ord__dict
   Orderings_preorder__dict
   Orderings_order__dict
   Orderings_linorder__dict
   HOL_equal__dict
 
 experiment begin
 
 embed (eval) test1 is
   Pairing__Heap__Tree_link
   Pairing__Heap__Tree_pass\<^sub>1
   Pairing__Heap__Tree_pass\<^sub>2
-  Pairing__Heap__Tree_merge__pairs
   Pairing__Heap__Tree_pheap
   .
 
 end
 
 end
diff --git a/thys/CakeML_Codegen/Utils/Test_Utils.thy b/thys/CakeML_Codegen/Utils/Test_Utils.thy
--- a/thys/CakeML_Codegen/Utils/Test_Utils.thy
+++ b/thys/CakeML_Codegen/Utils/Test_Utils.thy
@@ -1,136 +1,135 @@
 theory Test_Utils
 imports
   Code_Utils
   Huffman.Huffman
   "HOL-Data_Structures.Leftist_Heap"
   "Pairing_Heap.Pairing_Heap_Tree"
   "Root_Balanced_Tree.Root_Balanced_Tree"
   "Dict_Construction.Dict_Construction"
 begin
 
 section \<open>Dynamic unfolding\<close>
 
 definition one :: nat where
 "one = 1"
 
 fun plus_one :: "nat \<Rightarrow> nat" where
 "plus_one (Suc x) = one + plus_one x" |
 "plus_one _ = one"
 
 ML\<open>
 fun has_one ctxt =
   let
     val const = @{const_name plus_one}
     val {eqngr, ...} = Code_Preproc.obtain true {ctxt = ctxt, consts = [const], terms = []}
     val all_consts = Graph.all_succs eqngr [const]
   in
     member op = all_consts @{const_name one}
   end
 \<close>
 
 ML\<open>@{assert} (has_one @{context})\<close>
 
 context
   notes [[dynamic_unfold]]
 begin
 
 ML\<open>@{assert} (not (has_one @{context}))\<close>
 
 end
 
 section \<open>Pattern compatibility\<close>
 
 subsection \<open>Cannot deal with diagonal function\<close>
 
 fun diagonal :: "_ \<Rightarrow> _ \<Rightarrow> _ \<Rightarrow> nat" where
 "diagonal x True False = 1" |
 "diagonal False y True = 2" |
 "diagonal True False z = 3"
 
 code_thms diagonal
 
 code_thms Leftist_Heap.ltree
 
 context
   notes [[pattern_compatibility]]
 begin
 
 ML\<open>
   {ctxt = @{context}, consts = [@{const_name diagonal}], terms = []}
   |> can (Code_Preproc.obtain true)
   |> not
   |> @{assert}
 \<close>
 
 export_code huffman checking SML Scala
 
 export_code
   Leftist_Heap.ltree
   Leftist_Heap.node
   Leftist_Heap.merge
   Leftist_Heap.insert
   Leftist_Heap.del_min
   checking SML Scala
 
 export_code
   Pairing_Heap_Tree.link
   Pairing_Heap_Tree.pass\<^sub>1
   Pairing_Heap_Tree.pass\<^sub>2
-  Pairing_Heap_Tree.merge_pairs
   Pairing_Heap_Tree.is_root
   Pairing_Heap_Tree.pheap
   checking SML Scala
 
 export_code
   Root_Balanced_Tree.size_tree_tm
   Root_Balanced_Tree.inorder2_tm
   Root_Balanced_Tree.split_min_tm
   checking SML Scala
 
 end
 
 (* FIXME RBT *)
 
 (* FIXME move to Dict_Construction *)
 
 ML\<open>open Dict_Construction_Util\<close>
 
 lemma
   assumes "P" "Q" "R"
   shows "P \<and> Q \<and> R"
 apply (tactic \<open>
   (REPEAT_ALL_NEW (resolve_tac @{context} @{thms conjI}) CONTINUE_WITH
     [resolve_tac @{context} @{thms assms(1)}, resolve_tac @{context} @{thms assms(2)}, resolve_tac @{context} @{thms assms(3)}]) 1
 \<close>)
 done
 
 lemma
   assumes "P" "Q" "R"
   shows "P \<and> Q \<and> R"
 apply (tactic \<open>
   (REPEAT_ALL_NEW (resolve_tac @{context} @{thms conjI}) CONTINUE_WITH_FW
     [resolve_tac @{context} @{thms assms(1)}, K all_tac, resolve_tac @{context} @{thms assms(3)}]) 1
 \<close>)
 apply (rule assms(2))
 done
 
 lemma
   assumes "P" "Q"
   shows "(P \<and> Q)" "(P \<and> Q)"
 apply (tactic \<open>Goal.recover_conjunction_tac THEN
   (Goal.conjunction_tac THEN_ALL_NEW
     (REPEAT_ALL_NEW (resolve_tac @{context} @{thms conjI}) CONTINUE_WITH
     [resolve_tac @{context} @{thms assms(1)}, resolve_tac @{context} @{thms assms(2)}])) 1
 \<close>)
 done
 
 lemma
   assumes "Q" "P"
   shows "P \<and> Q"
 apply (tactic \<open>
   (resolve_tac @{context} @{thms conjI conjI[rotated]} CONTINUE_WITH
     [resolve_tac @{context} @{thms assms(1)}, resolve_tac @{context} @{thms assms(2)}]) 1
 \<close>)
 done
 
 end
\ No newline at end of file