dropped dead code;
authorhaftmann
Sun Nov 11 19:56:02 2012 +0100 (2012-11-11)
changeset 500460051dc4f301f
parent 50045 2214bc566f88
child 50047 45684acf0b94
child 50050 fac2b27893ff
dropped dead code;
tuned theory text
src/HOL/Quickcheck.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
     1.1 --- a/src/HOL/Quickcheck.thy	Sun Nov 11 19:24:01 2012 +0100
     1.2 +++ b/src/HOL/Quickcheck.thy	Sun Nov 11 19:56:02 2012 +0100
     1.3 @@ -157,11 +157,11 @@
     1.4        (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
     1.5  proof (induct i rule: code_numeral.induct)
     1.6    case zero
     1.7 -  show ?case by (subst select_weight_drop_zero[symmetric])
     1.8 -    (simp add: filter.simps random_aux_set.simps[simplified])
     1.9 +  show ?case by (subst select_weight_drop_zero [symmetric])
    1.10 +    (simp add: random_aux_set.simps [simplified])
    1.11  next
    1.12    case (Suc i)
    1.13 -  show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one)
    1.14 +  show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_code_numeral_minus_one)
    1.15  qed
    1.16  
    1.17  definition "random_set i = random_aux_set i i"
     2.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Sun Nov 11 19:24:01 2012 +0100
     2.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Nov 11 19:56:02 2012 +0100
     2.3 @@ -411,34 +411,6 @@
     2.4       Code_Evaluation.term_of (- (int_of i) div 2) else Code_Evaluation.term_of ((int_of i + 1) div 2))"
     2.5  by (rule partial_term_of_anything)+
     2.6  
     2.7 -text {* Defining integers by positive and negative copy of naturals *}
     2.8 -(*
     2.9 -datatype simple_int = Positive nat | Negative nat
    2.10 -
    2.11 -primrec int_of_simple_int :: "simple_int => int"
    2.12 -where
    2.13 -  "int_of_simple_int (Positive n) = int n"
    2.14 -| "int_of_simple_int (Negative n) = (-1 - int n)"
    2.15 -
    2.16 -instantiation int :: narrowing
    2.17 -begin
    2.18 -
    2.19 -definition narrowing_int :: "code_int => int cons"
    2.20 -where
    2.21 -  "narrowing_int d = map_cons int_of_simple_int ((narrowing :: simple_int narrowing) d)"
    2.22 -
    2.23 -instance ..
    2.24 -
    2.25 -end
    2.26 -
    2.27 -text {* printing the partial terms *}
    2.28 -
    2.29 -lemma [code]:
    2.30 -  "partial_term_of (ty :: int itself) t == Code_Evaluation.App (Code_Evaluation.Const (STR ''Quickcheck_Narrowing.int_of_simple_int'')
    2.31 -     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Quickcheck_Narrowing.simple_int'') [], Typerep.Typerep (STR ''Int.int'') []])) (partial_term_of (TYPE(simple_int)) t)"
    2.32 -by (rule partial_term_of_anything)
    2.33 -
    2.34 -*)
    2.35  
    2.36  subsection {* The @{text find_unused_assms} command *}
    2.37  
     3.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sun Nov 11 19:24:01 2012 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sun Nov 11 19:56:02 2012 +0100
     3.3 @@ -45,25 +45,6 @@
     3.4  val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true)
     3.5  val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (K true)
     3.6   
     3.7 -(** general term functions **)
     3.8 -
     3.9 -fun mk_measure f =
    3.10 -  let
    3.11 -    val Type ("fun", [T, @{typ nat}]) = fastype_of f 
    3.12 -  in
    3.13 -    Const (@{const_name Wellfounded.measure},
    3.14 -      (T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool})
    3.15 -    $ f
    3.16 -  end
    3.17 -
    3.18 -fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) =
    3.19 -  let
    3.20 -    val lt = mk_sumcases rT f TL
    3.21 -    val rt = mk_sumcases rT f TR
    3.22 -  in
    3.23 -    SumTree.mk_sumcase TL TR rT lt rt
    3.24 -  end
    3.25 -  | mk_sumcases _ f T = f T
    3.26  
    3.27  (** abstract syntax **)
    3.28  
    3.29 @@ -80,9 +61,6 @@
    3.30      Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y
    3.31    end
    3.32  
    3.33 -fun mk_unit_let (x, y) =
    3.34 -  Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ absdummy @{typ unit} y
    3.35 -
    3.36  fun mk_if (b, t, e) =
    3.37    let
    3.38      val T = fastype_of t
    3.39 @@ -100,7 +78,6 @@
    3.40  
    3.41  val exhaustiveN = "exhaustive";
    3.42  val full_exhaustiveN = "full_exhaustive";
    3.43 -val fast_exhaustiveN = "fast_exhaustive";
    3.44  val bounded_forallN = "bounded_forall";
    3.45  
    3.46  fun fast_exhaustiveT T = (T --> @{typ unit})
    3.47 @@ -145,20 +122,6 @@
    3.48      val bounds = map Bound (((length xs) - 1) downto 0)
    3.49      val start_term = test_function simpleT $ list_comb (constr, bounds)
    3.50    in fold_rev (fn f => fn t => f t) fns start_term end
    3.51 -      
    3.52 -fun mk_fast_equations functerms =
    3.53 -  let
    3.54 -    fun test_function T = Free ("f", T --> @{typ "unit"})
    3.55 -    val mk_call = gen_mk_call (fn T =>
    3.56 -      Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"},
    3.57 -        fast_exhaustiveT T))
    3.58 -    val mk_aux_call = gen_mk_aux_call functerms
    3.59 -    val mk_consexpr = gen_mk_consexpr test_function
    3.60 -    fun mk_rhs exprs = @{term "If :: bool => unit => unit => unit"}
    3.61 -        $ size_ge_zero $ (foldr1 mk_unit_let exprs) $ @{term "()"}
    3.62 -  in
    3.63 -    mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
    3.64 -  end
    3.65  
    3.66  fun mk_equations functerms =
    3.67    let
    3.68 @@ -228,26 +191,6 @@
    3.69      mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
    3.70    end
    3.71    
    3.72 -(** foundational definition with the function package **)
    3.73 -
    3.74 -val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
    3.75 -
    3.76 -fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
    3.77 -    Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
    3.78 -
    3.79 -fun mk_termination_measure T =
    3.80 -  let
    3.81 -    val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
    3.82 -  in
    3.83 -    mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
    3.84 -  end
    3.85 -
    3.86 -fun termination_tac ctxt = 
    3.87 -  Function_Relation.relation_tac ctxt mk_termination_measure 1
    3.88 -  THEN rtac @{thm wf_measure} 1
    3.89 -  THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
    3.90 -    (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
    3.91 -     @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
    3.92  
    3.93  (** instantiating generator classes **)
    3.94    
    3.95 @@ -278,10 +221,6 @@
    3.96   ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall},
    3.97     mk_bounded_forall_equations, bounded_forallT, ["P", "i"]);
    3.98  
    3.99 -val instantiate_fast_exhaustive_datatype = instantiate_datatype 
   3.100 - ("fast exhaustive generators", fast_exhaustiveN, @{sort fast_exhaustive},
   3.101 -   mk_fast_equations, fast_exhaustiveT, ["f", "i"])
   3.102 -
   3.103  val instantiate_exhaustive_datatype = instantiate_datatype  
   3.104    ("exhaustive generators", exhaustiveN, @{sort exhaustive},
   3.105      mk_equations, exhaustiveT, ["f", "i"])
   3.106 @@ -479,7 +418,7 @@
   3.107        Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
   3.108          $ lambda (Free (s, T)) t $ depth
   3.109      fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
   3.110 -    fun mk_let safe def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
   3.111 +    fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
   3.112      val mk_test_term =
   3.113        mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt
   3.114    in lambda depth (mk_test_term t) end
     4.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Nov 11 19:24:01 2012 +0100
     4.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Nov 11 19:56:02 2012 +0100
     4.3 @@ -126,8 +126,6 @@
     4.4  fun narrowingT T =
     4.5    @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T])
     4.6  
     4.7 -fun mk_empty T = Const (@{const_name Quickcheck_Narrowing.empty}, narrowingT T)
     4.8 -
     4.9  fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T)
    4.10  
    4.11  fun mk_apply (T, t) (U, u) =
    4.12 @@ -147,7 +145,7 @@
    4.13  
    4.14  (** deriving narrowing instances **)
    4.15  
    4.16 -fun mk_equations descr vs tycos narrowings (Ts, Us) =
    4.17 +fun mk_equations descr vs narrowings =
    4.18    let
    4.19      fun mk_call T =
    4.20        (T, Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T))
    4.21 @@ -188,7 +186,7 @@
    4.22        thy
    4.23        |> Class.instantiation (tycos, vs, @{sort narrowing})
    4.24        |> Quickcheck_Common.define_functions
    4.25 -        (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE)
    4.26 +        (fn narrowings => mk_equations descr vs narrowings, NONE)
    4.27          prfx [] narrowingsN (map narrowingT (Ts @ Us))
    4.28        |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    4.29      else
    4.30 @@ -221,15 +219,13 @@
    4.31    let val ({elapsed, ...}, result) = Timing.timing e ()
    4.32    in (result, (description, Time.toMilliseconds elapsed)) end
    4.33    
    4.34 -fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, value_name) =
    4.35 +fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) =
    4.36    let
    4.37      val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
    4.38      fun message s = if quiet then () else Output.urgent_message s
    4.39      fun verbose_message s = if not quiet andalso verbose then Output.urgent_message s else ()
    4.40      val current_size = Unsynchronized.ref 0
    4.41      val current_result = Unsynchronized.ref Quickcheck.empty_result 
    4.42 -    fun excipit () =
    4.43 -      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
    4.44      val tmp_prefix = "Quickcheck_Narrowing"
    4.45      val ghc_options = Config.get ctxt ghc_options
    4.46      val with_tmp_dir =
    4.47 @@ -262,7 +258,7 @@
    4.48            ghc_options ^ " " ^
    4.49            (space_implode " " (map File.shell_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
    4.50            " -o " ^ executable ^ ";"
    4.51 -        val (result, compilation_time) =
    4.52 +        val (_, compilation_time) =
    4.53            elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
    4.54          val _ = Quickcheck.add_timing compilation_time current_result
    4.55          fun haskell_string_of_bool v = if v then "True" else "False"
    4.56 @@ -357,7 +353,7 @@
    4.57      fun mk_eval_cfun dT rT =
    4.58        Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, 
    4.59          Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT)
    4.60 -    fun eval_function (T as Type (@{type_name fun}, [dT, rT])) =
    4.61 +    fun eval_function (Type (@{type_name fun}, [dT, rT])) =
    4.62        let
    4.63          val (rt', rT') = eval_function rT
    4.64        in
    4.65 @@ -433,7 +429,7 @@
    4.66  fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
    4.67      Datatype_Case.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
    4.68        (t, mk_case_term ctxt (p - 1) qs' c)) cs)
    4.69 -  | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) =
    4.70 +  | mk_case_term ctxt p ((@{const_name All}, _) :: qs') (Universal_Counterexample (t, c)) =
    4.71      if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
    4.72  
    4.73  val post_process = (perhaps (try Quickcheck_Common.post_process_term)) o eval_finite_functions
    4.74 @@ -443,11 +439,11 @@
    4.75      val
    4.76        ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs)
    4.77      in
    4.78 -      map (fn (p, (_, (x, T))) => (x, mk_case_term ctxt p qs result)) ps
    4.79 +      map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps
    4.80        |> map (apsnd post_process)
    4.81      end
    4.82    
    4.83 -fun test_term ctxt catch_code_errors (t, eval_terms) =
    4.84 +fun test_term ctxt catch_code_errors (t, _) =
    4.85    let
    4.86      fun dest_result (Quickcheck.Result r) = r 
    4.87      val opts =
     5.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Nov 11 19:24:01 2012 +0100
     5.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Nov 11 19:56:02 2012 +0100
     5.3 @@ -83,8 +83,6 @@
     5.4      val names = Term.add_free_names t []
     5.5      val current_size = Unsynchronized.ref 0
     5.6      val current_result = Unsynchronized.ref Quickcheck.empty_result 
     5.7 -    fun excipit () =
     5.8 -      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
     5.9      val act = if catch_code_errors then try else (fn f => SOME o f) 
    5.10      val (test_fun, comp_time) = cpu_time "quickcheck compilation"
    5.11          (fn () => act (compile ctxt) [(t, eval_terms)]);
    5.12 @@ -134,44 +132,6 @@
    5.13        in !current_result end
    5.14    end;
    5.15  
    5.16 -fun validate_terms ctxt ts =
    5.17 -  let
    5.18 -    val _ = map check_test_term ts
    5.19 -    val size = Config.get ctxt Quickcheck.size
    5.20 -    val (test_funs, comp_time) = cpu_time "quickcheck batch compilation"
    5.21 -      (fn () => Quickcheck.mk_batch_validator ctxt ts) 
    5.22 -    fun with_size tester k =
    5.23 -      if k > size then true
    5.24 -      else if tester k then with_size tester (k + 1) else false
    5.25 -    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
    5.26 -        Option.map (map (fn test_fun =>
    5.27 -          TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
    5.28 -              (fn () => with_size test_fun 1) ()
    5.29 -             handle TimeLimit.TimeOut => true)) test_funs)
    5.30 -  in
    5.31 -    (results, [comp_time, exec_time])
    5.32 -  end
    5.33 -  
    5.34 -fun test_terms ctxt ts =
    5.35 -  let
    5.36 -    val _ = map check_test_term ts
    5.37 -    val size = Config.get ctxt Quickcheck.size
    5.38 -    val namess = map (fn t => Term.add_free_names t []) ts
    5.39 -    val (test_funs, comp_time) =
    5.40 -      cpu_time "quickcheck batch compilation" (fn () => Quickcheck.mk_batch_tester ctxt ts) 
    5.41 -    fun with_size tester k =
    5.42 -      if k > size then NONE
    5.43 -      else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
    5.44 -    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
    5.45 -        Option.map (map (fn test_fun =>
    5.46 -          TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
    5.47 -              (fn () => with_size test_fun 1) ()
    5.48 -             handle TimeLimit.TimeOut => NONE)) test_funs)
    5.49 -  in
    5.50 -    (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results,
    5.51 -      [comp_time, exec_time])
    5.52 -  end
    5.53 -
    5.54  fun test_term_with_cardinality (name, (size_matters_for, compile)) ctxt catch_code_errors ts =
    5.55    let
    5.56      val genuine_only = Config.get ctxt Quickcheck.genuine_only
    5.57 @@ -294,7 +254,7 @@
    5.58  fun subtype_preprocess ctxt (T, (t, ts)) =
    5.59    let
    5.60      val preds = Subtype_Predicates.get (Context.Proof ctxt)
    5.61 -    fun matches (p $ x) = AList.defined Term.could_unify preds p  
    5.62 +    fun matches (p $ _) = AList.defined Term.could_unify preds p  
    5.63      fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p)
    5.64      fun subst_of (tyco, v as Free (x, repT)) =
    5.65        let
    5.66 @@ -330,9 +290,9 @@
    5.67            [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals
    5.68      val error_msg =
    5.69        cat_lines
    5.70 -        (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
    5.71 +        (maps (map_filter (fn (_, Term _) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
    5.72      fun is_wellsorted_term (T, Term t) = SOME (T, t)
    5.73 -      | is_wellsorted_term (_, Wellsorted_Error s) = NONE
    5.74 +      | is_wellsorted_term (_, Wellsorted_Error _) = NONE
    5.75      val correct_inst_goals =
    5.76        case map (map_filter is_wellsorted_term) inst_goals of
    5.77          [[]] => error error_msg
    5.78 @@ -498,7 +458,7 @@
    5.79    | make_set T1 ((t1, @{const True}) :: tps) =
    5.80      Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
    5.81        $ t1 $ (make_set T1 tps)
    5.82 -  | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
    5.83 +  | make_set T1 ((_, t) :: _) = raise TERM ("make_set", [t])
    5.84  
    5.85  fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
    5.86    | make_coset T tps = 
     6.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Nov 11 19:24:01 2012 +0100
     6.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Nov 11 19:56:02 2012 +0100
     6.3 @@ -42,7 +42,7 @@
     6.4    let
     6.5      val fun_upd = Const (@{const_name fun_upd},
     6.6        (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
     6.7 -    val ((y, t2), seed') = random seed;
     6.8 +    val ((_, t2), seed') = random seed;
     6.9      val (seed'', seed''') = random_split seed';
    6.10  
    6.11      val state = Unsynchronized.ref (seed'', [], fn () => Abs ("x", T1, t2 ()));
    6.12 @@ -62,10 +62,6 @@
    6.13      fun term_fun' () = #3 (! state) ();
    6.14    in ((random_fun', term_fun'), seed''') end;
    6.15  
    6.16 -fun mk_if (b, t, e) =
    6.17 -  let
    6.18 -    val T = fastype_of t
    6.19 -  in Const (@{const_name "HOL.If"}, @{typ bool} --> T --> T --> T) $ b $ t $ e end
    6.20    
    6.21  (** datatypes **)
    6.22  
    6.23 @@ -77,7 +73,6 @@
    6.24  val eq = Thm.cprop_of @{thm random_aux_rec} |> Thm.dest_arg |> Thm.dest_arg |> Thm.dest_arg;
    6.25  val lhs = eq |> Thm.dest_arg1;
    6.26  val pt_random_aux = lhs |> Thm.dest_fun;
    6.27 -val ct_k = lhs |> Thm.dest_arg;
    6.28  val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun;
    6.29  val aT = pt_random_aux |> Thm.ctyp_of_term |> dest_ctyp_nth 1;
    6.30  
    6.31 @@ -187,14 +182,13 @@
    6.32  
    6.33  val random_auxN = "random_aux";
    6.34  
    6.35 -fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
    6.36 +fun mk_random_aux_eqs thy descr vs (names, auxnames) (Ts, Us) =
    6.37    let
    6.38      val mk_const = curry (Sign.mk_const thy);
    6.39      val random_auxsN = map (prefix (random_auxN ^ "_")) (names @ auxnames);
    6.40      val rTs = Ts @ Us;
    6.41      fun random_resultT T = @{typ Random.seed}
    6.42        --> HOLogic.mk_prodT (termifyT T,@{typ Random.seed});
    6.43 -    val pTs = map random_resultT rTs;
    6.44      fun sizeT T = @{typ code_numeral} --> @{typ code_numeral} --> T;
    6.45      val random_auxT = sizeT o random_resultT;
    6.46      val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT))
    6.47 @@ -257,7 +251,7 @@
    6.48              $ HOLogic.mk_number @{typ code_numeral} l $ size
    6.49        | NONE => size;
    6.50      val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq
    6.51 -      (mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us));
    6.52 +      (mk_random_aux_eqs thy descr vs (names, auxnames) (Ts, Us));
    6.53      val random_defs = map_index (fn (k, T) => mk_prop_eq
    6.54        (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
    6.55    in
    6.56 @@ -294,7 +288,7 @@
    6.57  
    6.58  val target = "Quickcheck";
    6.59  
    6.60 -fun mk_generator_expr ctxt (t, eval_terms) =
    6.61 +fun mk_generator_expr ctxt (t, _) =
    6.62    let  
    6.63      val thy = Proof_Context.theory_of ctxt
    6.64      val prop = fold_rev absfree (Term.add_frees t []) t
    6.65 @@ -304,7 +298,7 @@
    6.66        (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
    6.67      val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
    6.68      val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
    6.69 -    val ([genuine_only_name], ctxt') = Variable.variant_fixes ["genuine_only"] ctxt
    6.70 +    val ([genuine_only_name], _) = Variable.variant_fixes ["genuine_only"] ctxt
    6.71      val genuine_only = Free (genuine_only_name, @{typ bool})
    6.72      val none_t = Const (@{const_name "None"}, resultT)
    6.73      val check = Quickcheck_Common.mk_safe_if genuine_only none_t (result, none_t,
    6.74 @@ -327,7 +321,7 @@
    6.75        (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
    6.76    end;
    6.77  
    6.78 -fun mk_reporting_generator_expr ctxt (t, eval_terms) =
    6.79 +fun mk_reporting_generator_expr ctxt (t, _) =
    6.80    let
    6.81      val thy = Proof_Context.theory_of ctxt
    6.82      val resultT = @{typ "(bool * term list) option * (bool list * bool)"}
    6.83 @@ -348,7 +342,7 @@
    6.84      fun mk_concl_report b =
    6.85        HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT (replicate (length assms) @{term True}),
    6.86          Quickcheck_Common.reflect_bool b)
    6.87 -    val ([genuine_only_name], ctxt') = Variable.variant_fixes ["genuine_only"] ctxt
    6.88 +    val ([genuine_only_name], _) = Variable.variant_fixes ["genuine_only"] ctxt
    6.89      val genuine_only = Free (genuine_only_name, @{typ bool})
    6.90      val none_t = HOLogic.mk_prod (@{term "None :: (bool * term list) option"}, mk_concl_report true)
    6.91      val concl_check = Quickcheck_Common.mk_safe_if genuine_only none_t (concl, none_t,
    6.92 @@ -422,7 +416,7 @@
    6.93            (fn proc => fn g => fn c => fn b => fn s => g c b s
    6.94              #>> (apfst o Option.map o apsnd o map) proc) t' [];
    6.95          fun single_tester c b s = compile c b s |> Random_Engine.run
    6.96 -        fun iterate_and_collect _ (card, size) 0 report = (NONE, report)
    6.97 +        fun iterate_and_collect _ _ 0 report = (NONE, report)
    6.98            | iterate_and_collect genuine_only (card, size) j report =
    6.99              let
   6.100                val (test_result, single_report) = apsnd Run (single_tester card genuine_only size)
   6.101 @@ -444,7 +438,7 @@
   6.102            (fn proc => fn g => fn c => fn b => fn s => g c b s
   6.103              #>> (Option.map o apsnd o map) proc) t' [];
   6.104          fun single_tester c b s = compile c b s |> Random_Engine.run
   6.105 -        fun iterate _ (card, size) 0 = NONE
   6.106 +        fun iterate _ _ 0 = NONE
   6.107            | iterate genuine_only (card, size) j =
   6.108              case single_tester card genuine_only size of
   6.109                NONE => iterate genuine_only (card, size) (j - 1)