src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

 fun map2_optional f (x :: xs) (y :: ys) = f x (SOME y) :: (map2_optional f xs ys)
   | map2_optional f (x :: xs) [] = (f x NONE) :: (map2_optional f xs [])
   | map2_optional f [] [] = []
 
 fun find_indices f xs =
-  map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs)
+  map_filter (fn (i, true) => SOME i | (_, false) => NONE) (map_index (apsnd f) xs)
 
 (* mode *)
 
 datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
 

           (map all_modes_of_typ' S) [Bool]
       else
         raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
     end
   | all_modes_of_typ @{typ bool} = [Bool]
-  | all_modes_of_typ T =
+  | all_modes_of_typ _ =
     raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
 
 fun all_smodes_of_typ (T as Type ("fun", _)) =
   let
     val (S, U) = strip_type T

   comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
   | map_filter_prod f t = f t
   
 fun split_modeT mode Ts =
   let
-    fun split_arg_mode (Fun _) T = ([], [])
+    fun split_arg_mode (Fun _) _ = ([], [])
       | split_arg_mode (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
         let
           val (i1, o1) = split_arg_mode m1 T1
           val (i2, o2) = split_arg_mode m2 T2
         in

     Const (c, _) => c = constname
   | _ => false) t)
   
 fun is_intro constname t = is_intro_term constname (prop_of t)
 
-fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT);
-
 fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
   | is_predT _ = false
 
 (*** check if a term contains only constructor functions ***)
 (* TODO: another copy in the core! *)

       | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
             (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
           | _ => false)
       | _ => false)
   in check end;
-
-fun is_funtype (Type ("fun", [_, _])) = true
-  | is_funtype _ = false;
-
-fun is_Type (Type _) = true
-  | is_Type _ = false
 
 (* returns true if t is an application of an datatype constructor *)
 (* which then consequently would be splitted *)
 (* else false *)
 (*

       (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head)
   end
 
 fun fold_atoms f intro s =
   let
-    val (literals, head) = Logic.strip_horn intro
+    val (literals, _) = Logic.strip_horn intro
     fun appl t s = (case t of
       (@{term Not} $ t') => f t' s
       | _ => f t s)
   in fold appl (map HOLogic.dest_Trueprop literals) s end
 

     val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
   in
     (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
   end;
 
-fun map_premises f intro =
-  let
-    val (premises, head) = Logic.strip_horn intro
-  in
-    Logic.list_implies (map f premises, head)
-  end
-
 fun map_filter_premises f intro =
   let
     val (premises, head) = Logic.strip_horn intro
   in
     Logic.list_implies (map_filter f premises, head)

 fun prepare_split_thm ctxt split_thm =
     (split_thm RS @{thm iffD2})
     |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
       @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
 
-fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype.info_of_case thy name)
+fun find_split_thm thy (Const (name, _)) = Option.map #split (Datatype.info_of_case thy name)
   | find_split_thm thy _ = NONE
 
 (* lifting term operations to theorems *)
 
 fun map_term thy f th =

 (** tuple processing **)
 
 fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
   | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
     (case HOLogic.strip_tupleT (fastype_of arg) of
-      (Ts as _ :: _ :: _) =>
+      (_ :: _ :: _) =>
       let
         fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
           (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
           | rewrite_arg' (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
             let

     singleton (Variable.export ctxt' ctxt) (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th)
   end
 
 fun dest_conjunct_prem th =
   case HOLogic.dest_Trueprop (prop_of th) of
-    (Const (@{const_name HOL.conj}, _) $ t $ t') =>
+    (Const (@{const_name HOL.conj}, _) $ _ $ _) =>
       dest_conjunct_prem (th RS @{thm conjunct1})
         @ dest_conjunct_prem (th RS @{thm conjunct2})
     | _ => [th]
 
 fun expand_tuples thy intro =
   let
     val ctxt = Proof_Context.init_global thy
     val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
     val intro_t = prop_of intro'
     val concl = Logic.strip_imp_concl intro_t
-    val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
+    val (_, args) = strip_comb (HOLogic.dest_Trueprop concl)
     val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
-    val (pats', intro_t', ctxt3) = 
-      fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
+    val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
     fun rewrite_pat (ct1, ct2) =
       (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
     val t_insts' = map rewrite_pat t_insts
     val intro'' = Thm.instantiate (T_insts, t_insts') intro
     val [intro'''] = Variable.export ctxt3 ctxt [intro'']

     fun instantiate th =
     let
       val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
       val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
       val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
-      val T = TFree (tname, HOLogic.typeS)
       val T' = TFree (tname', HOLogic.typeS)
       val U = TFree (uname, HOLogic.typeS)
       val y = Free (yname, U)
       val f' = absdummy (U --> T') (Bound 0 $ y)
       val th' = Thm.certify_instantiate

 fun imp_prems_conv cv ct =
   case Thm.term_of ct of
     Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   | _ => Conv.all_conv ct
 
-fun all_params_conv cv ctxt ct =
-  if Logic.is_all (Thm.term_of ct)
-  then Conv.arg_conv (Conv.abs_conv (all_params_conv cv o #2) ctxt) ct
-  else cv ctxt ct;
-  
 (** eta contract higher-order arguments **)
 
 fun eta_contract_ho_arguments thy intro =
   let
     fun f atom = list_comb (apsnd ((map o map_products) Envir.eta_contract) (strip_comb atom))

 fun import_intros inp_pred [] ctxt =
   let
     val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
     val T = fastype_of outp_pred
     val paramTs = ho_argsT_of_typ (binder_types T)
-    val (param_names, ctxt'') = Variable.variant_fixes
+    val (param_names, _) = Variable.variant_fixes
       (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
     val params = map2 (curry Free) param_names paramTs
   in
     (((outp_pred, params), []), ctxt')
   end

 (* defining a quickcheck predicate *)
 
 fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
   | strip_imp_prems _ = [];
 
-fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
-  | strip_imp_concl A = A : term;
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ _ $ B) = strip_imp_concl B
+  | strip_imp_concl A = A;
 
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
 
 fun define_quickcheck_predicate t thy =
   let