--- a/src/HOL/Induct/LList.thy Wed May 07 10:56:34 2008 +0200
+++ b/src/HOL/Induct/LList.thy Wed May 07 10:56:35 2008 +0200
@@ -566,7 +566,7 @@
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
@@ -574,7 +574,7 @@
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