# HG changeset patch
# User wenzelm
# Date 1159645167 -7200
# Node ID 1b43d9184bf59edc4ed02f6f27ea31108ef24b1c
# Parent  d3616b4abe1bdf18bc54d701775844758dfb9fa7
tuned proofs;

diff -r d3616b4abe1b -r 1b43d9184bf5 src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Sat Sep 30 21:39:25 2006 +0200
+++ b/src/HOL/Library/Coinductive_List.thy	Sat Sep 30 21:39:27 2006 +0200
@@ -170,10 +170,10 @@
     CONS (Datatype_Universe.Leaf x) (Rep_llist l)"
   by (simp add: LCons_def Abs_llist_inverse CONS_type Rep_llist)
 
-lemma llist_cases [case_names LNil LCons, cases type: llist]:
-  assumes LNil: "l = LNil \<Longrightarrow> C"
-    and LCons: "\<And>x l'. l = LCons x l' \<Longrightarrow> C"
-  shows C
+lemma llist_cases [cases type: llist]:
+  obtains
+    (LNil) "l = LNil"
+  | (LCons) x l' where "l = LCons x l'"
 proof (cases l)
   case (Abs_llist L)
   from `L \<in> llist` have "L \<in> LList (range Datatype_Universe.Leaf)" by (rule llistD)