1.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Sep 19 16:18:33 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Sep 19 16:18:34 2011 +0200
     1.3 @@ -29,14 +29,19 @@
     1.4  
     1.5  -- Answers
     1.6  
     1.7 -answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
     1.8 -answer a known unknown =
     1.9 +answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
    1.10 +answeri a known unknown =
    1.11    try (evaluate a) >>= (\res ->
    1.12       case res of
    1.13         Right b -> known b
    1.14         Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
    1.15         Left e -> throw e);
    1.16  
    1.17 +answer :: Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
    1.18 +answer a known unknown =
    1.19 +  Control.Exception.catch (answeri a known unknown) 
    1.20 +    (\ (PatternMatchFail _) -> known True);
    1.21 +
    1.22  -- Refute
    1.23  
    1.24  str_of_list [] = "[]";

     2.1 --- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Mon Sep 19 16:18:33 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Mon Sep 19 16:18:34 2011 +0200
     2.3 @@ -48,14 +48,19 @@
     2.4  
     2.5  data Answer = Known Bool | Unknown Pos deriving Show;
     2.6  
     2.7 -answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b
     2.8 -answer a known unknown =
     2.9 +answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
    2.10 +answeri a known unknown =
    2.11    do res <- try (evaluate a)
    2.12       case res of
    2.13         Right b -> known b
    2.14         Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
    2.15         Left e -> throw e
    2.16  
    2.17 +answer :: Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
    2.18 +answer a known unknown =
    2.19 +  Control.Exception.catch (answeri a known unknown) 
    2.20 +    (\ (PatternMatchFail _) -> known True)
    2.21 +
    2.22  --  Proofs and Refutation
    2.23  
    2.24  data Quantifier = ExistentialQ | UniversalQ