removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions
authorbulwahn
Thu, 08 Dec 2011 13:53:27 +0100
changeset 45789 36ea69266e61
parent 45788 9049b24959de
child 45790 3355c27c93a4
removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions
src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Dec 08 13:46:04 2011 +0100
+++ b/src/HOL/List.thy	Thu Dec 08 13:53:27 2011 +0100
@@ -5312,12 +5312,6 @@
 code_const dropWhile
   (Haskell "dropWhile")
 
-code_const hd
-  (Haskell "head")
-
-code_const last
-  (Haskell "last")
-
 code_const list_all
   (Haskell "all")