diff --git a/src/HOL/Data_Structures/Tree23_of_List.thy b/src/HOL/Data_Structures/Tree23_of_List.thy
--- a/src/HOL/Data_Structures/Tree23_of_List.thy
+++ b/src/HOL/Data_Structures/Tree23_of_List.thy
@@ -1,178 +1,178 @@
 (* Author: Tobias Nipkow *)
 
 section \<open>2-3 Tree from List\<close>
 
 theory Tree23_of_List
 imports Tree23
 begin
 
 text \<open>Linear-time bottom up conversion of a list of items into a complete 2-3 tree
 whose inorder traversal yields the list of items.\<close>
 
 
 subsection "Code"
 
 text \<open>Nonempty lists of 2-3 trees alternating with items, starting and ending with a 2-3 tree:\<close>
 
 datatype 'a tree23s = T "'a tree23" | TTs "'a tree23" "'a" "'a tree23s"
 
 abbreviation "not_T ts == (\<forall>t. ts \<noteq> T t)"
 
 fun len :: "'a tree23s \<Rightarrow> nat" where
 "len (T _) = 1" |
 "len (TTs _ _ ts) = len ts + 1"
 
-fun trees :: "'a tree23s \<Rightarrow> 'a tree23 list" where
-"trees (T t) = [t]" |
-"trees (TTs t a ts) = t # trees ts"
+fun trees :: "'a tree23s \<Rightarrow> 'a tree23 set" where
+"trees (T t) = {t}" |
+"trees (TTs t a ts) = {t} \<union> trees ts"
 
 text \<open>Join pairs of adjacent trees:\<close>
 
 fun join_adj :: "'a tree23s \<Rightarrow> 'a tree23s" where
 "join_adj (TTs t1 a (T t2)) = T(Node2 t1 a t2)" |
 "join_adj (TTs t1 a (TTs t2 b (T t3))) = T(Node3 t1 a t2 b t3)" |
 "join_adj (TTs t1 a (TTs t2 b tas)) = TTs (Node2 t1 a t2) b (join_adj tas)"
 
 text \<open>Towards termination of \<open>join_all\<close>:\<close>
 
 lemma len_ge2:
   "not_T ts \<Longrightarrow> len ts \<ge> 2"
 by(cases ts rule: join_adj.cases) auto
 
 lemma [measure_function]: "is_measure len"
 by(rule is_measure_trivial)
 
 lemma len_join_adj_div2:
   "not_T ts \<Longrightarrow> len(join_adj ts) \<le> len ts div 2"
 by(induction ts rule: join_adj.induct) auto
 
 lemma len_join_adj1: "not_T ts \<Longrightarrow> len(join_adj ts) < len ts"
 using len_join_adj_div2[of ts] len_ge2[of ts] by simp
 
 corollary len_join_adj2[termination_simp]: "len(join_adj (TTs t a ts)) \<le> len ts"
 using len_join_adj1[of "TTs t a ts"] by simp
 
 fun join_all :: "'a tree23s \<Rightarrow> 'a tree23" where
 "join_all (T t) = t" |
 "join_all tas = join_all (join_adj tas)"
 
 fun leaves :: "'a list \<Rightarrow> 'a tree23s" where
 "leaves [] = T Leaf" |
 "leaves (a # as) = TTs Leaf a (leaves as)"
 
 definition tree23_of_list :: "'a list \<Rightarrow> 'a tree23" where
 "tree23_of_list as = join_all(leaves as)"
 
 
 subsection \<open>Functional correctness\<close>
 
 subsubsection \<open>\<open>inorder\<close>:\<close>
 
 fun inorder2 :: "'a tree23s \<Rightarrow> 'a list" where
 "inorder2 (T t) = inorder t" |
 "inorder2 (TTs t a ts) = inorder t @ a # inorder2 ts"
 
 lemma inorder2_join_adj: "not_T ts \<Longrightarrow> inorder2(join_adj ts) = inorder2 ts"
 by (induction ts rule: join_adj.induct) auto
 
 lemma inorder_join_all: "inorder (join_all ts) = inorder2 ts"
 proof (induction ts rule: measure_induct_rule[where f = "len"])
   case (less ts)
   show ?case
   proof (cases ts)
     case T thus ?thesis by simp
   next
     case (TTs t a ts)
     then show ?thesis using less inorder2_join_adj[of "TTs t a ts"]
       by (simp add: le_imp_less_Suc len_join_adj2)
   qed
 qed
 
 lemma inorder2_leaves: "inorder2(leaves as) = as"
 by(induction as) auto
 
 lemma "inorder(tree23_of_list as) = as"
 by(simp add: tree23_of_list_def inorder_join_all inorder2_leaves)
 
 subsubsection \<open>Completeness:\<close>
 
 lemma complete_join_adj:
-  "\<forall>t \<in> set(trees ts). complete t \<and> height t = n \<Longrightarrow> not_T ts \<Longrightarrow>
-   \<forall>t \<in> set(trees (join_adj ts)). complete t \<and> height t = Suc n"
+  "\<forall>t \<in> trees ts. complete t \<and> height t = n \<Longrightarrow> not_T ts \<Longrightarrow>
+   \<forall>t \<in> trees (join_adj ts). complete t \<and> height t = Suc n"
 by (induction ts rule: join_adj.induct) auto
 
 lemma complete_join_all:
- "\<forall>t \<in> set(trees ts). complete t \<and> height t = n \<Longrightarrow> complete (join_all ts)"
+ "\<forall>t \<in> trees ts. complete t \<and> height t = n \<Longrightarrow> complete (join_all ts)"
 proof (induction ts arbitrary: n rule: measure_induct_rule[where f = "len"])
   case (less ts)
   show ?case
   proof (cases ts)
     case T thus ?thesis using less.prems by simp
   next
     case (TTs t a ts)
     then show ?thesis
       using less.prems apply simp
       using complete_join_adj[of "TTs t a ts" n, simplified] less.IH len_join_adj1 by blast
   qed
 qed
 
-lemma complete_leaves: "t \<in> set(trees (leaves as)) \<Longrightarrow> complete t \<and> height t = 0"
+lemma complete_leaves: "t \<in> trees (leaves as) \<Longrightarrow> complete t \<and> height t = 0"
 by (induction as) auto
 
 corollary complete: "complete(tree23_of_list as)"
 by(simp add: tree23_of_list_def complete_leaves complete_join_all[of _ 0])
 
 
 subsection "Linear running time"
 
 fun t_join_adj :: "'a tree23s \<Rightarrow> nat" where
 "t_join_adj (TTs t1 a (T t2)) = 1" |
 "t_join_adj (TTs t1 a (TTs t2 b (T t3))) = 1" |
 "t_join_adj (TTs t1 a (TTs t2 b ts)) = t_join_adj ts + 1"
 
 fun t_join_all :: "'a tree23s \<Rightarrow> nat" where
 "t_join_all (T t) = 1" |
 "t_join_all ts = t_join_adj ts + t_join_all (join_adj ts)"
 
 fun t_leaves :: "'a list \<Rightarrow> nat" where
 "t_leaves [] = 1" |
 "t_leaves (a # as) = t_leaves as + 1"
 
 definition t_tree23_of_list :: "'a list \<Rightarrow> nat" where
 "t_tree23_of_list as = t_leaves as + t_join_all(leaves as)"
 
 lemma t_join_adj: "not_T ts \<Longrightarrow> t_join_adj ts \<le> len ts div 2"
 by(induction ts rule: t_join_adj.induct) auto
 
 lemma t_join_all: "t_join_all ts \<le> len ts"
 proof(induction ts rule: measure_induct_rule[where f = len])
   case (less ts)
   show ?case
   proof (cases ts)
     case T thus ?thesis by simp
   next
     case TTs
     have 0: "\<forall>t. ts \<noteq> T t" using TTs by simp
     have "t_join_all ts = t_join_adj ts + t_join_all (join_adj ts)"
       using TTs by simp
     also have "\<dots> \<le> len ts div 2 + t_join_all (join_adj ts)"
       using t_join_adj[OF 0] by linarith
     also have "\<dots> \<le> len ts div 2 + len (join_adj ts)"
       using less.IH[of "join_adj ts"] len_join_adj1[OF 0] by simp
     also have "\<dots> \<le> len ts div 2 + len ts div 2"
       using len_join_adj_div2[OF 0] by linarith
     also have "\<dots> \<le> len ts" by linarith
     finally show ?thesis .
   qed
 qed
 
 lemma t_leaves: "t_leaves as = length as + 1"
 by(induction as) auto
 
 lemma len_leaves: "len(leaves as) = length as + 1"
 by(induction as) auto
 
 lemma t_tree23_of_list: "t_tree23_of_list as \<le> 2*(length as + 1)"
 using t_join_all[of "leaves as"] by(simp add: t_tree23_of_list_def t_leaves len_leaves)
 
 end
diff --git a/src/HOL/Data_Structures/document/root.bib b/src/HOL/Data_Structures/document/root.bib
--- a/src/HOL/Data_Structures/document/root.bib
+++ b/src/HOL/Data_Structures/document/root.bib
@@ -1,112 +1,122 @@
 @techreport{Adams-TR92,author="Stephen Adams",
 title="Implementing Sets Efficiently in a Functional Language",
 institution="University of Southampton, Department of Electronics and Computer Science",number="CSTR 92-10",year=1992}
 
 @article{Adams-JFP93,
   author    = {Stephen Adams},
   title     = {Efficient Sets - {A} Balancing Act},
   journal   = {J. Funct. Program.},
   volume    = {3},
   number    = {4},
   pages     = {553--561},
   year      = {1993}
 }
 
 @inproceedings{Andersson-WADS93,author={Arne Andersson},
 title={Balanced search trees made simple},pages={60--71},year=1993,
 booktitle={Algorithms and Data Structures (WADS '93)},
 series={LNCS},volume={709},publisher={Springer}}
 
 @inproceedings{BlellochFS-SPAA16,
   author    = {Guy E. Blelloch and
                Daniel Ferizovic and
                Yihan Sun},
   title     = {Just Join for Parallel Ordered Sets},
   booktitle = {{SPAA}},
   pages     = {253--264},
   publisher = {{ACM}},
   year      = {2016}
 }
 
 @unpublished{BraunRem,author={W. Braun and Martin Rem},
 title="A logarithmic implementation of flexible arrays",
 note="Memorandum MR83/4. Eindhoven University of Techology",year=1983}
 
 @phdthesis{Crane72,author={Clark A. Crane},
 title={Linear Lists and Prorty Queues as Balanced Binary Trees},
 school={Computer Science Department, Stanford University},year=1972}
 
 @article{Hinze-bro12,author={Ralf Hinze},
 title={Purely Functional 1-2 Brother Trees},
 journal={J. Functional Programming},
 volume=19,number={6},pages={633--644},year=2009}
 
+@article{jfp/Hinze18,
+  author    = {Ralf Hinze},
+  title     = {On constructing 2-3 trees},
+  journal   = {J. Funct. Program.},
+  volume    = {28},
+  pages     = {e19},
+  year      = {2018},
+  url       = {https://doi.org/10.1017/S0956796818000187},
+}
+
 @article{HoffmannOD-TOPLAS82,
 author={Christoph M. Hoffmann and Michael J. O'Donnell},
 title={Programming with Equations},journal={{ACM} Trans. Program. Lang. Syst.},
 volume=4,number=1,pages={83--112},year=1982}}
 
 @inproceedings{Hoogerwoord,author={Rob R. Hoogerwoord},
 title="A logarithmic implementation of flexible arrays",
 editor={R. Bird and C. Morgan and J. Woodcock},
 booktitle={Mathematics of Program Construction, Second International Conference},
 publisher={Springer},series={LNCS},volume=669,year=1992,
 pages={191-207}}
 
 @article{Kahrs-JFP01,author={Stefan Kahrs},title={Red-Black Trees with Types},
 journal={J. Functional Programming},volume=11,number=4,pages={425-432},year=2001}
 
 @misc{Kahrs-html,author={Stefan Kahrs},title={Red Black Trees},
 note={\url{http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html}}}
 
 @unpublished{Nipkow16,author={Tobias Nipkow},
 title={Automatic Functional Correctness Proofs for Functional Search Trees},
 year=2016,month=feb,note={\url{http://www.in.tum.de/~nipkow/pubs/trees.html}}}
 
 @inproceedings{NunezPP95,
   author    = {Manuel N{\'{u}}{\~{n}}ez and
                Pedro Palao and
                Ricardo Pena},
   title     = {A Second Year Course on Data Structures Based on Functional Programming},
   booktitle = {Functional Programming Languages in Education},
   pages     = {65--84},
   year      = {1995},
   editor    = {Pieter H. Hartel and
                Marinus J. Plasmeijer},
   series    = {LNCS},
   volume    = {1022},
   publisher = {Springer},
   year      = {1995},
 }
 
 
 @book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
 publisher="Cambridge University Press",year=1998}
 
 @article{OttmannS76,author={Thomas Ottmann and Hans-Werner Six},
 title={Eine neue {K}lasse von ausgeglichenen {B}in\"arb\"aumen},
 journal={Angewandte Informatik},volume=18,number=9,pages={395--400},year=1976}
 
 @article{OttmannW-CJ80,author={Thomas Ottmann and Derick Wood},
 title={1-2 Brother Trees or {AVL} Trees Revisited},journal={Comput. J.},
 volume=23,number=3,pages={248--255},year=1980}
 
 @inproceedings{Ragde14,author={Prabhakar Ragde},
 title={Simple Balanced Binary Search Trees},pages={78--87},year=2014,
 booktitle={Trends in Functional Programming in Education},
 series={EPTCS},volume=170,editor={Caldwell and H\"olzenspies and Achten}}
 
 @article{Reade-SCP92,author={Chris Reade},
 title={Balanced Trees with Removals: An Exercise in Rewriting and Proof},
 journal={Sci. Comput. Program.},volume=18,number=2,pages={181--204},year=1992}
 
 @article{Schoenmakers-IPL93,author="Berry Schoenmakers",
 title="A Systematic Analysis of Splaying",journal={Information Processing Letters},volume=45,pages={41-50},year=1993}
 
 @article{SleatorT-JACM85,author={Daniel D. Sleator and Robert E. Tarjan},
 title={Self-adjusting Binary Search Trees},journal={J. ACM},
 volume=32,number=3,pages={652-686},year=1985}
 
 @misc{Turbak230,author={Franklyn Turbak},
 title={{CS230 Handouts --- Spring 2007}},year=2007,
 note={\url{http://cs.wellesley.edu/~cs230/spring07/handouts.html}}}
diff --git a/src/HOL/Data_Structures/document/root.tex b/src/HOL/Data_Structures/document/root.tex
--- a/src/HOL/Data_Structures/document/root.tex
+++ b/src/HOL/Data_Structures/document/root.tex
@@ -1,80 +1,80 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage{latexsym}
 \usepackage{amssymb}
 \usepackage{amsmath}
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % snip
 \newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
 \newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
 
 \urlstyle{rm}
 \isabellestyle{it}
 
 \renewcommand{\isacharunderscore}{\_}
 \renewcommand{\isacharunderscorekeyword}{\_}
 
 % for uniform font size
 \renewcommand{\isastyle}{\isastyleminor}
 
 \begin{document}
 
 \title{Functional Data Structures}
 \author{Tobias Nipkow}
 \maketitle
 
 \begin{abstract}
 A collection of verified functional data structures. The emphasis is on
 conciseness of algorithms and succinctness of proofs, more in the style
 of a textbook than a library of efficient algorithms.
 
 For more details see \cite{Nipkow16}.
 \end{abstract}
 
 \setcounter{tocdepth}{1}
 \tableofcontents
 \newpage
 
 \input{session}
 
 \section{Bibliographic Notes}
 
 \paragraph{Red-black trees}
 The insert function follows Okasaki \cite{Okasaki}. The delete function
 in theory \isa{RBT\_Set} follows Kahrs \cite{Kahrs-html,Kahrs-JFP01},
 an alternative delete function is given in theory \isa{RBT\_Set2}.
 
 \paragraph{2-3 trees}
 Equational definitions were given by Hoffmann and
 O'Donnell~\cite{HoffmannOD-TOPLAS82} (only insertion)
 and Reade \cite{Reade-SCP92}.
 Our formalisation is based on the teaching material by
-Turbak~\cite{Turbak230} .
+Turbak~\cite{Turbak230}  and the article by Hinze~\cite{jfp/Hinze18}.
 
 \paragraph{1-2 brother trees}
 They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}.
 The functional version is due to Hinze~\cite{Hinze-bro12}.
 
 \paragraph{AA trees}
 They were invented by Arne Anderson \cite{Andersson-WADS93}.
 Our formalisation follows Ragde~\cite{Ragde14} but fixes a number
 of mistakes.
 
 \paragraph{Splay trees}
 They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
 Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
 
 \paragraph{Join-based BSTs}
 They were invented by Adams \cite{Adams-TR92,Adams-JFP93}
 and analyzed by Blelloch \emph{et al.} \cite{BlellochFS-SPAA16}.
 
 \paragraph{Leftist heaps}
 They were invented by Crane \cite{Crane72}. A first functional implementation
 is due to N\'u\~{n}ez \emph{et al.}~\cite{NunezPP95}.
 
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}