--- a/src/HOL/Data_Structures/Brother12_Set.thy Sat Mar 05 23:05:07 2016 +0100
+++ b/src/HOL/Data_Structures/Brother12_Set.thy Sun Mar 06 10:33:34 2016 +0100
@@ -160,7 +160,7 @@
subsubsection "Proofs for insertion"
lemma inorder_n1: "inorder(n1 t) = inorder t"
-by(induction t rule: n1.induct) (auto simp: sorted_lems)
+by(cases t rule: n1.cases) (auto simp: sorted_lems)
context insert
begin
@@ -190,7 +190,7 @@
by(cases t) auto
lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
-by(induction l a r rule: n2.induct) (auto)
+by(cases "(l,a,r)" rule: n2.cases) (auto)
lemma inorder_del_min:
"t \<in> T h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>