# HG changeset patch
# User wenzelm
# Date 1680431653 -7200
# Node ID 1f990c8bb74cb10686f8bd96ec46e4303f9a5480
# Parent  5d3ce9f96cfdfd7a66f66c626c140b749202e172# Parent  99a18dcff0109d1c7abdc26ebb77b5547f2db9ee
merged

diff -r 99a18dcff010 -r 1f990c8bb74c src/HOL/Data_Structures/Tries_Binary.thy
--- a/src/HOL/Data_Structures/Tries_Binary.thy	Sat Apr 01 21:33:54 2023 +0200
+++ b/src/HOL/Data_Structures/Tries_Binary.thy	Sun Apr 02 12:34:13 2023 +0200
@@ -138,12 +138,12 @@
 "insertP ks LfP  = NdP ks True (LfP,LfP)" |
 "insertP ks (NdP ps b lr) =
   (case split ks ps of
-     (qs,k#ks',p#ps') \<Rightarrow>
+     (qs, k#ks', p#ps') \<Rightarrow>
        let tp = NdP ps' b lr; tk = NdP ks' True (LfP,LfP) in
        NdP qs False (if k then (tp,tk) else (tk,tp)) |
-     (qs,k#ks',[]) \<Rightarrow>
+     (qs, k#ks', []) \<Rightarrow>
        NdP ps b (mod2 (insertP ks') k lr) |
-     (qs,[],p#ps') \<Rightarrow>
+     (qs, [], p#ps') \<Rightarrow>
        let t = NdP ps' b lr in
        NdP qs True (if p then (LfP,t) else (t,LfP)) |
      (qs,[],[]) \<Rightarrow> NdP ps True lr)"
@@ -156,9 +156,9 @@
 "deleteP ks LfP  = LfP" |
 "deleteP ks (NdP ps b lr) =
   (case split ks ps of
-     (qs,ks',p#ps') \<Rightarrow> NdP ps b lr |
-     (qs,k#ks',[]) \<Rightarrow> nodeP ps b (mod2 (deleteP ks') k lr) |
-     (qs,[],[]) \<Rightarrow> nodeP ps False lr)"
+     (_, _, _#_) \<Rightarrow> NdP ps b lr |
+     (_, k#ks', []) \<Rightarrow> nodeP ps b (mod2 (deleteP ks') k lr) |
+     (_, [], []) \<Rightarrow> nodeP ps False lr)"
 
 
 subsubsection \<open>Functional Correctness\<close>