src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML

 structure Predicate_Compile_Pred : PREDICATE_COMPILE_PRED =
 struct
 
 open Predicate_Compile_Aux
 
-fun is_compound ((Const (@{const_name Not}, _)) $ t) =
+fun is_compound ((Const (@{const_name Not}, _)) $ _) =
     error "is_compound: Negation should not occur; preprocessing is defect"
   | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
   | is_compound ((Const (@{const_name HOL.disj}, _)) $ _ $ _) = true
   | is_compound ((Const (@{const_name HOL.conj}, _)) $ _ $ _) =
     error "is_compound: Conjunction should not occur; preprocessing is defect"

       val split_thm = prepare_split_thm (Proof_Context.init_global thy) raw_split_thm
       (* TODO: contextify things - this line is to unvarify the split_thm *)
       (*val ((_, [isplit_thm]), _) =
         Variable.import true [split_thm] (Proof_Context.init_global thy)*)
       val (assms, concl) = Logic.strip_horn (prop_of split_thm)
-      val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
+      val (_, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
       val atom' = case_betapply thy atom
       val subst = Pattern.match thy (split_t, atom') (Vartab.empty, Vartab.empty)
       val names' = Term.add_free_names atom' names
       fun mk_subst_rhs assm =
         let

         val frees = Term.add_free_names rhs []
         val disjuncts = HOLogic.dest_disj rhs
         val nctxt = Name.make_context frees
         fun mk_introrule t =
           let
-            val ((ps, t'), nctxt') = focus_ex t nctxt
+            val ((ps, t'), _) = focus_ex t nctxt
             val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t')
           in
             (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
           end
         val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o

       val full_spec = (constname, intros') :: flat intross
       (*val thy''' = Predicate_Compile_Data.store_processed_specs (constname, full_spec) thy''*)
     in
       (full_spec, thy'')
     end;
-
-fun preprocess_term t thy = error "preprocess_pred_term: to implement" 
-
-fun is_Abs (Abs _) = true
-  | is_Abs _       = false
 
 fun flat_higher_order_arguments (intross, thy) =
   let
     fun process constname atom (new_defs, thy) =
       let