tuned

--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Jan 20 09:28:50 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Jan 20 09:28:51 2012 +0100
@@ -68,7 +68,7 @@
 
 fun mk_none_continuation (x, y) =
   let
-    val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
+    val (T as Type(@{type_name "option"}, _)) = fastype_of x
   in
     Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y
   end
@@ -131,12 +131,11 @@
    (T, fn t => nth functerms k $ absdummy T t $ size_pred)
   end
 
-fun gen_mk_consexpr test_function functerms simpleT (c, xs) =
+fun gen_mk_consexpr test_function simpleT (c, xs) =
   let
     val (Ts, fns) = split_list xs
     val constr = Const (c, Ts ---> simpleT)
     val bounds = map Bound (((length xs) - 1) downto 0)
-    val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
     val start_term = test_function simpleT $ list_comb (constr, bounds)
   in fold_rev (fn f => fn t => f t) fns start_term end
       
@@ -147,7 +146,7 @@
       Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"},
         fast_exhaustiveT T))
     val mk_aux_call = gen_mk_aux_call functerms
-    val mk_consexpr = gen_mk_consexpr test_function functerms
+    val mk_consexpr = gen_mk_consexpr test_function
     fun mk_rhs exprs = @{term "If :: bool => unit => unit => unit"}
         $ size_ge_zero $ (foldr1 mk_unit_let exprs) $ @{term "()"}
   in
@@ -160,7 +159,7 @@
     val mk_call = gen_mk_call (fn T =>
       Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T))
     val mk_aux_call = gen_mk_aux_call functerms
-    val mk_consexpr = gen_mk_consexpr test_function functerms
+    val mk_consexpr = gen_mk_consexpr test_function
     fun mk_rhs exprs =
       mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name "None"}, resultT))
   in
@@ -174,7 +173,7 @@
       Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
         bounded_forallT T))
     val mk_aux_call = gen_mk_aux_call functerms
-    val mk_consexpr = gen_mk_consexpr test_function functerms
+    val mk_consexpr = gen_mk_consexpr test_function
     fun mk_rhs exprs =
       mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term "True"})
   in
@@ -207,7 +206,6 @@
         val (Ts, fns) = split_list xs
         val constr = Const (c, Ts ---> simpleT)
         val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
-        val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
         val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
         val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
         val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
@@ -311,12 +309,11 @@
 
 fun mk_fast_generator_expr ctxt (t, eval_terms) =
   let
-    val thy = Proof_Context.theory_of ctxt
     val ctxt' = Variable.auto_fixes t ctxt
     val names = Term.add_free_names t []
     val frees = map Free (Term.add_frees t [])
     fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
-    val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+    val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt'
     val depth = Free (depth_name, @{typ code_numeral})
     fun return _ = @{term "throw_Counterexample :: term list => unit"} $
       (HOLogic.mk_list @{typ "term"}
@@ -340,12 +337,11 @@
 
 fun mk_generator_expr ctxt (t, eval_terms) =
   let
-    val thy = Proof_Context.theory_of ctxt
     val ctxt' = Variable.auto_fixes t ctxt
     val names = Term.add_free_names t []
     val frees = map Free (Term.add_frees t [])
     fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
-    val ([depth_name, genuine_only_name], ctxt'') =
+    val ([depth_name, genuine_only_name], _) =
       Variable.variant_fixes ["depth", "genuine_only"] ctxt'
     val depth = Free (depth_name, @{typ code_numeral})
     val genuine_only = Free (genuine_only_name, @{typ bool}) 
@@ -367,9 +363,9 @@
     val frees = map Free (Term.add_frees t [])
     val ([depth_name, genuine_only_name], ctxt'') =
       Variable.variant_fixes ["depth", "genuine_only"] ctxt'
-    val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt''
+    val (term_names, _) = Variable.variant_fixes (map (prefix "t_") names) ctxt''
     val depth = Free (depth_name, @{typ code_numeral})
-    val genuine_only = Free (depth_name, @{typ bool})    
+    val genuine_only = Free (genuine_only_name, @{typ bool})    
     val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
     fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
     val return = mk_return (HOLogic.mk_list @{typ term}
@@ -397,12 +393,11 @@
 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
     val ctxt' = Variable.auto_fixes t ctxt
     val names = Term.add_free_names t []
     val frees = map Free (Term.add_frees t [])
     fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
-    val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+    val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt'
     val depth = Free (depth_name, @{typ code_numeral})
     fun mk_bounded_forall (Free (s, T)) t =
       Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)