# HG changeset patch
# User wenzelm
# Date 1537723077 -7200
# Node ID e0d14f648d46c1361c3c00261fd1b5f41014efb9
# Parent  51005671bee545e54adcdddddc9335ec0ebc0733
eliminated old-style inner comments;

diff -r 51005671bee5 -r e0d14f648d46 src/HOL/Data_Structures/Tree234_Map.thy
--- a/src/HOL/Data_Structures/Tree234_Map.thy	Sun Sep 23 17:14:06 2018 +0200
+++ b/src/HOL/Data_Structures/Tree234_Map.thy	Sun Sep 23 19:17:57 2018 +0200
@@ -66,7 +66,7 @@
    GT \<Rightarrow> (case cmp x (fst ab3) of
             LT \<Rightarrow> (case upd x y t3 of
                     T\<^sub>i t3' \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3' ab3 t4)
-                  | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2(*q*) (Node3 t31 q t32 ab3 t4)) |
+                  | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2\<^cancel>\<open>q\<close> (Node3 t31 q t32 ab3 t4)) |
             EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 (x,y) t4) |
             GT \<Rightarrow> (case upd x y t4 of
                     T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4')