diff -r 66df76dd2640 -r 07906fc6af7a src/HOL/Quotient_Examples/Lift_DList.thy
--- a/src/HOL/Quotient_Examples/Lift_DList.thy	Tue Feb 25 15:02:19 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Tue Feb 25 15:02:20 2014 +0100
@@ -45,19 +45,7 @@
 
 lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr .
 
-lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat"
-proof -
-  {
-    fix x y
-    have "list_all2 cr_dlist x y \<Longrightarrow> x = List.map list_of_dlist y"
-      unfolding list_all2_iff cr_dlist_def by (induction x y rule: list_induct2') auto
-  }
-  note cr = this
-  fix x :: "'a list list" and y :: "'a list list"
-  assume "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y"
-  then have "x = y" by (auto dest: cr simp add: Lifting.invariant_def)
-  then show "?thesis x y" unfolding Lifting.invariant_def by auto
-qed
+lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat" by auto
 
 text {* We can export code: *}