# HG changeset patch
# User bulwahn
# Date 1323429663 -3600
# Node ID 331ebffe0593a3210cfcbbcc93977bd7c45a1ef0
# Parent  4096351375cc757763a371fe7c565215a53c028f
deactivating quickcheck_narrowing if Efficient_Nat theory is loaded

diff -r 4096351375cc -r 331ebffe0593 src/HOL/Library/Efficient_Nat.thy
--- 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 *}