# HG changeset patch
# User nipkow
# Date 870421339 -7200
# Node ID 8f9ee0f79d9ad4b191900ee47f55b0802de43c0f
# Parent  5a47b869d16a44fa2650a57529d75b0d9b8f2a7f
Corected bug in def of dropWhile (also present in Haskell lib!)

diff -r 5a47b869d16a -r 8f9ee0f79d9a src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Aug 01 09:41:38 1997 +0200
+++ b/src/HOL/List.thy	Fri Aug 01 09:42:19 1997 +0200
@@ -108,7 +108,7 @@
   "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
 primrec dropWhile list
   "dropWhile P [] = []"
-  "dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)"
+  "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
 
 end