src/HOL/Induct/LList.thy

 lemma Lmap_compose: "M \<in> llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)"
 apply (simp add: o_def)
 apply (drule imageI)
 apply (erule LList_equalityI, safe)
 apply (erule llist.cases, simp_all)
-apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
+apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ f])+
 apply assumption  
 done
 
 lemma Lmap_ident: "M \<in> llist(A) ==> Lmap (%x. x) M = M"
 apply (drule imageI)
 apply (erule LList_equalityI, safe)
 apply (erule llist.cases, simp_all)
-apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
+apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ "%x. x"])+
 apply assumption 
 done
 
 
 subsection{* @{text Lappend} -- its two arguments cause some complications! *}