src/HOL/Library/Efficient_Nat.thy
changeset 45793 331ebffe0593
parent 45185 3a0c63c0ed48
child 46028 9f113cdf3d66
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Dec 09 12:21:01 2011 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Dec 09 12:21:03 2011 +0100
@@ -412,6 +412,12 @@
 code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term"
   (SML "HOLogic.mk'_number/ HOLogic.natT")
 
+text {* Evaluation with @{text "Quickcheck_Narrowing"} does not work, as
+  @{text "code_module"} is very aggressive leading to bad Haskell code.
+  Therefore, we simply deactivate the narrowing-based quickcheck from here on.
+*}
+
+declare [[quickcheck_narrowing_active = false]] 
 
 text {* Module names *}