1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Dec 09 12:21:01 2011 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Dec 09 12:21:03 2011 +0100
     1.3 @@ -412,6 +412,12 @@
     1.4  code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term"
     1.5    (SML "HOLogic.mk'_number/ HOLogic.natT")
     1.6  
     1.7 +text {* Evaluation with @{text "Quickcheck_Narrowing"} does not work, as
     1.8 +  @{text "code_module"} is very aggressive leading to bad Haskell code.
     1.9 +  Therefore, we simply deactivate the narrowing-based quickcheck from here on.
    1.10 +*}
    1.11 +
    1.12 +declare [[quickcheck_narrowing_active = false]] 
    1.13  
    1.14  text {* Module names *}
    1.15