1.1 --- a/src/HOL/Library/Quickcheck_Narrowing.thy	Mon Mar 14 12:34:08 2011 +0100
     1.2 +++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Mon Mar 14 12:34:09 2011 +0100
     1.3 @@ -4,7 +4,8 @@
     1.4  
     1.5  theory Quickcheck_Narrowing
     1.6  imports Main "~~/src/HOL/Library/Code_Char"
     1.7 -uses ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
     1.8 +uses
     1.9 +  ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
    1.10  begin
    1.11  
    1.12  subsection {* Counterexample generator *}

     2.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Mar 14 12:34:08 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Mar 14 12:34:09 2011 +0100
     2.3 @@ -89,9 +89,9 @@
     2.4    property app = P $ \n d -> Result [] [] (app . reverse);
     2.5  };
     2.6  
     2.7 -instance (Term_of a, Serial a, Testable b) => Testable (a -> b) where {
     2.8 +instance (Term_of a, Narrowing a, Testable b) => Testable (a -> b) where {
     2.9    property f = P $ \n d ->
    2.10 -    let C t c = series d
    2.11 +    let C t c = narrowing d
    2.12          c' = conv c
    2.13          r = run (\(x:xs) -> f xs (c' x)) (n+1) d
    2.14      in  r { args = Var [n] t : args r, showArgs = (show . term_of . c') : showArgs r };

     3.1 --- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Mar 14 12:34:08 2011 +0100
     3.2 +++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Mar 14 12:34:09 2011 +0100
     3.3 @@ -115,12 +115,12 @@
     3.4                   
     3.5  subsection {* Necessary instantiation for quickcheck generator *}
     3.6  
     3.7 -instantiation tree :: (serial) serial
     3.8 +instantiation tree :: (narrowing) narrowing
     3.9  begin
    3.10  
    3.11 -function series_tree
    3.12 +function narrowing_tree
    3.13  where
    3.14 -  "series_tree d = sum (cons ET) (apply (apply (apply (apply (cons MKT) series) series_tree) series_tree) series) d"
    3.15 +  "narrowing_tree d = sum (cons ET) (apply (apply (apply (apply (cons MKT) narrowing) narrowing_tree) narrowing_tree) narrowing) d"
    3.16  by pat_completeness auto
    3.17  
    3.18  termination proof (relation "measure nat_of")