src/HOL/Library/Coinductive_List.thy

   then have h': "\<And>x. h' x =
       (case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h' w))"
     unfolding h'_def by (simp add: LList_corec)
   have "(h x, h' x) \<in> {(h u, h' u) | u. True}" by blast
   then show "h x = h' x"
-  proof (coinduct rule: LList_equalityI [where A = UNIV])
+  proof (coinduct taking: UNIV rule: LList_equalityI)
     case (EqLList M N)
     then obtain x where MN: "M = h x" "N = h' x" by blast
     show ?case
     proof (cases "f x")
       case None

 proof -
   def M \<equiv> "Rep_llist l1" and N \<equiv> "Rep_llist l2"
   with r have "(M, N) \<in> {(Rep_llist l1, Rep_llist l2) | l1 l2. (l1, l2) \<in> r}"
     by blast
   then have "M = N"
-  proof (coinduct rule: LList_equalityI [where A = UNIV])
+  proof (coinduct taking: UNIV rule: LList_equalityI)
     case (EqLList M N)
     then obtain l1 l2 where
         MN: "M = Rep_llist l1" "N = Rep_llist l2" and r: "(l1, l2) \<in> r"
       by auto
     from step [OF r] show ?case

   shows "Lmap (f o g) M = Lmap f (Lmap g M)"  (is "?lhs M = ?rhs M")
 proof -
   have "(?lhs M, ?rhs M) \<in> {(?lhs N, ?rhs N) | N. N \<in> LList A}"
     using M by blast
   then show ?thesis
-  proof (coinduct taking: "range (\<lambda>N :: 'a Datatype.item. N)"
-      rule: LList_equalityI)
+  proof (coinduct taking: "range (\<lambda>N. N)" rule: LList_equalityI)
     case (EqLList L M)
     then obtain N where LM: "L = ?lhs N" "M = ?rhs N" and N: "N \<in> LList A" by blast
     from N show ?case
     proof cases
       case NIL

   assumes M: "M \<in> LList A"
   shows "Lmap (\<lambda>x. x) M = M"  (is "?lmap M = _")
 proof -
   have "(?lmap M, M) \<in> {(?lmap N, N) | N. N \<in> LList A}" using M by blast
   then show ?thesis
-  proof (coinduct taking: "range (\<lambda>N :: 'a Datatype.item. N)"
-      rule: LList_equalityI)
+  proof (coinduct taking: "range (\<lambda>N. N)" rule: LList_equalityI)
     case (EqLList L M)
     then obtain N where LM: "L = ?lmap N" "M = N" and N: "N \<in> LList A" by blast
     from N show ?case
     proof cases
       case NIL