src/HOL/Tools/Quickcheck/quickcheck_common.ML
changeset 45724 1f5fc44254d7
parent 45721 d1fb55c2ed65
child 45728 123e3a9a3bb3
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -274,7 +274,7 @@
   @{term "Quickcheck.catch_match :: (bool * term list) option => (bool * term list) option => (bool * term list) option"}
     $ (@{term "If :: bool => (bool * term list) option => (bool * term list) option => (bool * term list) option"}
       $ cond $ then_t $ else_t true)
-    $ (if Config.get ctxt Quickcheck.potential then else_t false else @{term "None :: term list option"});  
+    $ (if Config.get ctxt Quickcheck.potential then else_t false else @{term "None :: (bool * term list) option"});
 
 fun collect_results f [] results = results
   | collect_results f (t :: ts) results =