src/HOL/Tools/Quickcheck/exhaustive_generators.ML

 
 exception FUNCTION_TYPE;
 
 exception Counterexample of term list
 
+val resultT =  @{typ "(bool * term list) option"};
+
 val exhaustiveN = "exhaustive";
 val full_exhaustiveN = "full_exhaustive";
 val fast_exhaustiveN = "fast_exhaustive";
 val bounded_forallN = "bounded_forall";
 

 fun exhaustiveT T = (T --> @{typ "Code_Evaluation.term list option"})
   --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
 
 fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
 
-fun full_exhaustiveT T = (termifyT T --> @{typ "(bool * Code_Evaluation.term list) option"})
-  --> @{typ code_numeral} --> @{typ "(bool * Code_Evaluation.term list) option"}
-
-fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
-  --> @{typ "Code_Evaluation.term list option"}
+fun full_exhaustiveT T = (termifyT T --> resultT) --> @{typ code_numeral} --> resultT
+
+fun check_allT T = (termifyT T --> resultT) --> resultT
 
 fun mk_equation_terms generics (descr, vs, Ts) =
   let
     val (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, exhaustives) = generics
     val rhss =

     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   end
   
 fun mk_full_equations functerms =
   let
-    fun test_function T = Free ("f", termifyT T --> @{typ "(bool * term list) option"})
+    fun test_function T = Free ("f", termifyT T --> resultT)
+    fun split_const T = HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, resultT)
     fun mk_call T =
       let
         val full_exhaustive =
           Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
             full_exhaustiveT T)
       in                                   
         (T, fn t => full_exhaustive $
-          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"},
-            @{typ "(bool * Code_Evaluation.term list) option"})
-          $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
+          (split_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
       end
     fun mk_aux_call fTs (k, _) (tyco, Ts) =
       let
         val T = Type (tyco, Ts)
         val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
       in
         (T, fn t => nth functerms k $
-          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"},
-            @{typ "(bool * Code_Evaluation.term list) option"})
-            $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
+          (split_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
       end
     fun mk_consexpr simpleT (c, xs) =
       let
         val (Ts, fns) = split_list xs
         val constr = Const (c, Ts ---> simpleT)

         (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
           $ (list_comb (constr, bounds)) $ absdummy @{typ unit} term)
       in fold_rev (fn f => fn t => f t) fns start_term end
     fun mk_rhs exprs =
       mk_if (size_ge_zero, foldr1 mk_none_continuation exprs,
-        @{term "None :: (bool * term list) option"})
+        Const (@{const_name "None"}, resultT))
   in
     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   end
   
 (** foundational definition with the function package **)

         (HOLogic.mk_list @{typ term}
           (map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms)))
     fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
       if Sign.of_sort thy (T, @{sort enum}) then
         Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
-          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
+          $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT) 
             $ lambda free (lambda term_var t))
       else
         Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
-          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "(bool * term list) option"})
+          $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
             $ lambda free (lambda term_var t)) $ depth
-    val none_t = @{term "None :: (bool * term list) option"}
+    val none_t = Const (@{const_name "None"}, resultT)
     val mk_if = Quickcheck_Common.mk_safe_if ctxt
     val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
   in lambda depth (mk_test_term t) end
 
 fun mk_parametric_generator_expr mk_generator_expr =
   Quickcheck_Common.gen_mk_parametric_generator_expr 
-    ((mk_generator_expr, absdummy @{typ "code_numeral"} @{term "None :: (bool * term list) option"}),
-      @{typ "code_numeral => (bool * term list) option"})
+    ((mk_generator_expr, absdummy @{typ "code_numeral"} (Const (@{const_name "None"}, resultT))),
+      @{typ "code_numeral"} --> resultT)
 
 fun mk_validator_expr ctxt t =
   let
     fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
     val thy = Proof_Context.theory_of ctxt