# HG changeset patch
# User haftmann
# Date 1352759080 -3600
# Node ID 72efd6b4038d5f4f4baabdb8eedeac4629e67b76
# Parent  94041d602ecb32eae883ac642da111b3cfd0a7a5
dropped dead code

diff -r 94041d602ecb -r 72efd6b4038d src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Mon Nov 12 23:24:40 2012 +0100
@@ -212,8 +212,7 @@
     fun PEEK f dependent_tactic st = dependent_tactic (f st) st
     fun meta_eq_of th = th RS @{thm eq_reflection}
     val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
-    fun instantiate i n {context = ctxt, params = p, prems = prems,
-      asms = a, concl = cl, schematics = s}  =
+    fun instantiate i n {context, params, prems, asms, concl, schematics} =
       let
         fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
         fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
@@ -293,10 +292,10 @@
 
 fun add_intro (opt_case_name, thm) thy =
   let
-    val (name, T) = dest_Const (fst (strip_intro_concl thm))
+    val (name, _) = dest_Const (fst (strip_intro_concl thm))
     fun cons_intro gr =
      case try (Graph.get_node gr) name of
-       SOME pred_data => Graph.map_node name (map_pred_data
+       SOME _ => Graph.map_node name (map_pred_data
          (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
      | NONE => Graph.new_node (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr
   in PredData.map cons_intro thy end
@@ -386,9 +385,6 @@
         val pred = Const (name, Sign.the_const_type thy name)
         val ctxt = Proof_Context.init_global thy
         val elim_t = mk_casesrule ctxt pred (map snd named_intros')
-        val nparams = (case try (Inductive.the_inductive ctxt) name of
-            SOME (_, result) => length (Inductive.params_of (#raw_induct result))
-          | NONE => 0)
         val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
       in
         ((named_intros', SOME elim'), true)
@@ -417,7 +413,7 @@
     (* thm refl is a dummy thm *)
     val modes = map fst compilations
     val (needs_random, non_random_modes) = pairself (map fst)
-      (List.partition (fn (m, (fun_name, random)) => random) compilations)
+      (List.partition (fn (_, (_, random)) => random) compilations)
     val non_random_dummys = map (rpair "dummy") non_random_modes
     val all_dummys = map (rpair "dummy") modes
     val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
diff -r 94041d602ecb -r 72efd6b4038d src/HOL/Tools/Predicate_Compile/mode_inference.ML
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Mon Nov 12 23:24:40 2012 +0100
@@ -60,13 +60,6 @@
 datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
   | Mode_Pair of mode_derivation * mode_derivation | Term of mode
 
-fun string_of_derivation (Mode_App (m1, m2)) =
-  "App (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
-  | string_of_derivation (Mode_Pair (m1, m2)) =
-  "Pair (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
-  | string_of_derivation (Term m) = "Term (" ^ string_of_mode m ^ ")"
-  | string_of_derivation (Context m) = "Context (" ^ string_of_mode m ^ ")"
-
 fun strip_mode_derivation deriv =
   let
     fun strip (Mode_App (deriv1, deriv2)) ds = strip deriv1 (deriv2 :: ds)
@@ -118,43 +111,20 @@
     (Syntax.string_of_term ctxt t) ^ "(sidecondition)"
   | string_of_prem ctxt _ = raise Fail "string_of_prem: unexpected input"
 
-fun string_of_clause ctxt pred (ts, prems) =
-  (space_implode " --> "
-  (map (string_of_prem ctxt) prems)) ^ " --> " ^ pred ^ " "
-   ^ (space_implode " " (map (Syntax.string_of_term ctxt) ts))
-
 type mode_analysis_options =
   {use_generators : bool,
   reorder_premises : bool,
   infer_pos_and_neg_modes : bool}
 
-fun is_constrt thy =
-  let
-    val cnstrs = flat (maps
-      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
-      (Symtab.dest (Datatype.get_all thy)));
-    fun check t = (case strip_comb t of
-        (Free _, []) => true
-      | (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;
-
 (*** check if a type is an equality type (i.e. doesn't contain fun)
   FIXME this is only an approximation ***)
 fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
   | is_eqT _ = true;
 
-fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
+fun term_vs tm = fold_aterms (fn Free (x, _) => cons x | _ => I) tm [];
 val terms_vs = distinct (op =) o maps term_vs;
 
-(** collect all Frees in a term (with duplicates!) **)
-fun term_vTs tm =
-  fold_aterms (fn Free xT => cons xT | _ => I) tm [];
-
-fun print_failed_mode options thy modes p (pol, m) rs is =
+fun print_failed_mode options p (_, m) is =
   if show_mode_inference options then
     let
       val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
@@ -162,7 +132,7 @@
     in () end
   else ()
 
-fun error_of p (pol, m) is =
+fun error_of p (_, m) is =
   "  Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
         p ^ " violates mode " ^ string_of_mode m
 
@@ -195,27 +165,10 @@
     fold find' xs NONE
   end
   
-fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
-val terms_vs = distinct (op =) o maps term_vs;
-
-fun input_mode T =
-  let
-    val (Ts, U) = strip_type T
-  in
-    fold_rev (curry Fun) (map (K Input) Ts) Input
-  end
-
-fun output_mode T =
-  let
-    val (Ts, U) = strip_type T
-  in
-    fold_rev (curry Fun) (map (K Output) Ts) Output
-  end
-
 fun is_invertible_function ctxt (Const (f, _)) = is_constr ctxt f
   | is_invertible_function ctxt _ = false
 
-fun non_invertible_subterms ctxt (t as Free _) = []
+fun non_invertible_subterms ctxt (Free _) = []
   | non_invertible_subterms ctxt t = 
   let
     val (f, args) = strip_comb t
@@ -281,7 +234,7 @@
   | output_terms (t, Term Output) = [t]
   | output_terms _ = []
 
-fun lookup_mode modes (Const (s, T)) =
+fun lookup_mode modes (Const (s, _)) =
    (case (AList.lookup (op =) modes s) of
       SOME ms => SOME (map (fn m => (Context m, [])) ms)
     | NONE => NONE)
@@ -312,7 +265,7 @@
     end*)
     (case try (all_derivations_of ctxt modes vs) t  of
       SOME derivs =>
-        filter (fn (d, mvars) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
+        filter (fn (d, _) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
     | NONE => (if is_all_input m then [(Context m, [])] else []))
   | derivations_of ctxt modes vs t m =
     if eq_mode (m, Input) then
@@ -353,7 +306,7 @@
     SOME (s, _) =>
       (case AList.lookup (op =) modes s of
         SOME ms =>
-          (case AList.lookup (op =) (map (fn ((p, m), r) => (m, r)) ms) (head_mode_of deriv) of
+          (case AList.lookup (op =) (map (fn ((_, m), r) => (m, r)) ms) (head_mode_of deriv) of
             SOME r => r
           | NONE => false)
       | NONE => false)
@@ -370,21 +323,16 @@
     length (filter contains_output args)
   end
 
-fun lex_ord ord1 ord2 (x, x') =
-  case ord1 (x, x') of
-    EQUAL => ord2 (x, x')
-  | ord => ord
-
 fun lexl_ord [] (x, x') = EQUAL
   | lexl_ord (ord :: ords') (x, x') =
     case ord (x, x') of
       EQUAL => lexl_ord ords' (x, x')
     | ord => ord
 
-fun deriv_ord' ctxt pol pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
+fun deriv_ord' ctxt _ pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
   let
     (* prefer functional modes if it is a function *)
-    fun fun_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+    fun fun_ord ((t1, deriv1, _), (t2, deriv2, _)) =
       let
         fun is_functional t mode =
           case try (fst o dest_Const o fst o strip_comb) t of
@@ -398,20 +346,20 @@
         | (false, false) => EQUAL
       end
     (* prefer modes without requirement for generating random values *)
-    fun mvars_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+    fun mvars_ord ((_, _, mvars1), (_, _, mvars2)) =
       int_ord (length mvars1, length mvars2)
     (* prefer non-random modes *)
-    fun random_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+    fun random_mode_ord ((t1, deriv1, _), (t2, deriv2, _)) =
       int_ord (if random_mode_in_deriv modes t1 deriv1 then 1 else 0,
                if random_mode_in_deriv modes t2 deriv2 then 1 else 0)
     (* prefer modes with more input and less output *)
-    fun output_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+    fun output_mode_ord ((_, deriv1, _), (_, deriv2, _)) =
       int_ord (number_of_output_positions (head_mode_of deriv1),
         number_of_output_positions (head_mode_of deriv2))
     (* prefer recursive calls *)
     fun is_rec_premise t =
-      case fst (strip_comb t) of Const (c, T) => c = pred | _ => false
-    fun recursive_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+      case fst (strip_comb t) of Const (c, _) => c = pred | _ => false
+    fun recursive_ord ((t1, _, _), (t2, deriv2, _)) =
       int_ord (if is_rec_premise t1 then 0 else 1,
         if is_rec_premise t2 then 0 else 1)
     val ord = lexl_ord [mvars_ord, fun_ord, random_mode_ord, output_mode_ord, recursive_ord]
@@ -424,10 +372,6 @@
 fun premise_ord thy pol pred modes ((prem1, a1), (prem2, a2)) =
   rev_option_ord (deriv_ord' thy pol pred modes (dest_indprem prem1) (dest_indprem prem2)) (a1, a2)
 
-fun print_mode_list modes =
-  tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
-    commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
-
 fun select_mode_prem (mode_analysis_options : mode_analysis_options) (ctxt : Proof.context) pred
   pol (modes, (pos_modes, neg_modes)) vs ps =
   let
@@ -435,7 +379,7 @@
           find_least (deriv_ord ctxt pol pred modes t) (all_derivations_of ctxt pos_modes vs t)
       | choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
       | choose_mode_of_prem (Negprem t) = find_least (deriv_ord ctxt (not pol) pred modes t)
-          (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
+          (filter (fn (d, _) => is_all_input (head_mode_of d))
              (all_derivations_of ctxt neg_modes vs t))
       | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: unexpected premise " ^ string_of_prem ctxt p)
   in
@@ -451,17 +395,16 @@
     val vTs = distinct (op =) (fold Term.add_frees (map dest_indprem ps) (fold Term.add_frees ts []))
     val modes' = modes @ (param_vs ~~ map (fn x => [((true, x), false), ((false, x), false)]) (ho_arg_modes_of mode))
     fun retrieve_modes_of_pol pol = map (fn (s, ms) =>
-      (s, map_filter (fn ((p, m), r) => if p = pol then SOME m else NONE | _ => NONE) ms))
+      (s, map_filter (fn ((p, m), _) => if p = pol then SOME m else NONE | _ => NONE) ms))
     val (pos_modes', neg_modes') =
       if #infer_pos_and_neg_modes mode_analysis_options then
         (retrieve_modes_of_pol pol modes', retrieve_modes_of_pol (not pol) modes')
       else
         let
-          val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
+          val modes = map (fn (s, ms) => (s, map (fn ((_, m), _) => m) ms)) modes'
         in (modes, modes) end
     val (in_ts, out_ts) = split_mode mode ts
     val in_vs = union (op =) param_vs (maps (vars_of_destructable_term ctxt) in_ts)
-    val out_vs = terms_vs out_ts
     fun known_vs_after p vs = (case p of
         Prem t => union (op =) vs (term_vs t)
       | Sidecond t => union (op =) vs (term_vs t)
@@ -480,7 +423,7 @@
                 (distinct (op =) missing_vars))
                 @ acc_ps) true (known_vs_after p vs) (filter_out (equal p) ps)
           else NONE
-        | SOME (p, NONE) => NONE
+        | SOME (_, NONE) => NONE
         | NONE => NONE)
   in
     case check_mode_prems [] false in_vs ps of
@@ -508,7 +451,7 @@
     fun split xs =
       let
         fun split' [] (ys, zs) = (rev ys, rev zs)
-          | split' ((m, Error z) :: xs) (ys, zs) = split' xs (ys, z :: zs)
+          | split' ((_, Error z) :: xs) (ys, zs) = split' xs (ys, z :: zs)
           | split' (((m : bool * mode), Success rnd) :: xs) (ys, zs) = split' xs ((m, rnd) :: ys, zs)
        in
          split' xs ([], [])
@@ -522,7 +465,7 @@
         cond_timeit false "aux part of check_mode for one mode" (fn _ => 
         case find_indices is_none res of
           [] => Success (exists (fn SOME (_, _, true) => true | _ => false) res)
-        | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)))
+        | is => (print_failed_mode options p m is; Error (error_of p m is)))
       end
     val _ = if show_mode_inference options then
         tracing ("checking " ^ string_of_int (length ms) ^ " modes ...")
@@ -537,9 +480,9 @@
   let
     val rs = these (AList.lookup (op =) clauses p)
   in
-    (p, map (fn (m, rnd) =>
+    (p, map (fn (m, _) =>
       (m, map
-        ((fn (ts, ps, rnd) => (ts, ps)) o the o
+        ((fn (ts, ps, _) => (ts, ps)) o the o
           check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)) ms)
   end;
 
@@ -567,18 +510,12 @@
 fun infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt
   preds all_modes param_vs clauses =
   let
-    fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
     fun add_needs_random s (false, m) = ((false, m), false)
       | add_needs_random s (true, m) = ((true, m), needs_random s m)
     fun add_polarity_and_random_bit s b ms = map (fn m => add_needs_random s (b, m)) ms
     val prednames = map fst preds
     (* extramodes contains all modes of all constants, should we only use the necessary ones
        - what is the impact on performance? *)
-    fun predname_of (Prem t) =
-        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
-      | predname_of (Negprem t) =
-        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
-      | predname_of _ = I
     val relevant_prednames = fold (fn (_, clauses') =>
       fold (fn (_, ps) => fold Term.add_const_names (map dest_indprem ps)) clauses') clauses []
       |> filter_out (fn name => member (op =) prednames name)
diff -r 94041d602ecb -r 72efd6b4038d src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Nov 12 23:24:40 2012 +0100
@@ -157,7 +157,7 @@
         map (apsnd (map fst)) proposed_modes,
       proposed_names =
         maps (fn (predname, ms) => (map_filter
-          (fn (m, NONE) => NONE | (m, SOME name) => SOME ((predname, m), name))) ms) proposed_modes,
+          (fn (_, NONE) => NONE | (m, SOME name) => SOME ((predname, m), name))) ms) proposed_modes,
       show_steps = chk "show_steps",
       show_intermediate_results = chk "show_intermediate_results",
       show_proof_trace = chk "show_proof_trace",
diff -r 94041d602ecb -r 72efd6b4038d src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Nov 12 23:24:40 2012 +0100
@@ -931,7 +931,7 @@
     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 ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
       val T' = TFree (tname', HOLogic.typeS)
       val U = TFree (uname, HOLogic.typeS)
       val y = Free (yname, U)
diff -r 94041d602ecb -r 72efd6b4038d src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Mon Nov 12 23:24:40 2012 +0100
@@ -89,20 +89,20 @@
 fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if},
   HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
 
-fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
+fun mk_iterate_upto _ _ = error "not implemented yet"
 
 fun mk_not t =
   let
     val T = mk_monadT HOLogic.unitT
   in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end
 
-fun mk_Enum f = error "not implemented"
+fun mk_Enum _ = error "not implemented"
 
-fun mk_Eval (f, x) = error "not implemented"
+fun mk_Eval _ = error "not implemented"
 
-fun dest_Eval t = error "not implemented"
+fun dest_Eval _ = error "not implemented"
 
-fun mk_map T1 T2 tf tp = error "not implemented"
+fun mk_map _ _ _ _ = error "not implemented"
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
@@ -138,7 +138,7 @@
 fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
   HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
 
-fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
+fun mk_iterate_upto _ _ = error "not implemented yet"
 
 fun mk_not t =
   let
@@ -148,13 +148,13 @@
     val T = mk_monadT HOLogic.unitT
   in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end
 
-fun mk_Enum f = error "not implemented"
+fun mk_Enum _ = error "not implemented"
 
-fun mk_Eval (f, x) = error "not implemented"
+fun mk_Eval _ = error "not implemented"
 
-fun dest_Eval t = error "not implemented"
+fun dest_Eval _ = error "not implemented"
 
-fun mk_map T1 T2 tf tp = error "not implemented"
+fun mk_map _ _ _ _ = error "not implemented"
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
@@ -193,7 +193,7 @@
 fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if},
   HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
 
-fun mk_iterate_upto T (f, from, to) = error "not implemented"
+fun mk_iterate_upto _ _ = error "not implemented"
 
 fun mk_not t =
   let
@@ -202,13 +202,13 @@
       --> @{typ "code_numeral => (bool * Code_Evaluation.term list) option"}
   in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end
 
-fun mk_Enum f = error "not implemented"
+fun mk_Enum _ = error "not implemented"
 
-fun mk_Eval (f, x) = error "not implemented"
+fun mk_Eval _ = error "not implemented"
 
-fun dest_Eval t = error "not implemented"
+fun dest_Eval _ = error "not implemented"
 
-fun mk_map T1 T2 tf tp = error "not implemented"
+fun mk_map _ _ _ _  = error "not implemented"
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
@@ -296,7 +296,7 @@
 fun mk_if cond = Const (@{const_name DSequence.if_seq},
   HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
 
-fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
 fun mk_not t = let val T = mk_dseqT HOLogic.unitT
   in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
@@ -347,7 +347,7 @@
 fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq},
   HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
 
-fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
 fun mk_not t =
   let
@@ -408,7 +408,7 @@
 fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq},
   HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
 
-fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
 fun mk_not t =
   let
@@ -599,7 +599,7 @@
 fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
   HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
 
-fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
 fun mk_not t =
   let
diff -r 94041d602ecb -r 72efd6b4038d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Nov 12 23:24:40 2012 +0100
@@ -80,20 +80,6 @@
             HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
   in mk_eqs x xs end;
 
-fun mk_scomp (t, u) =
-  let
-    val T = fastype_of t
-    val U = fastype_of u
-    val [A] = binder_types T
-    val D = body_type U                   
-  in 
-    Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
-  end;
-
-fun dest_randomT (Type ("fun", [@{typ Random.seed},
-  Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
-  | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
-
 fun mk_tracing s t =
   Const(@{const_name Code_Evaluation.tracing},
     @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
@@ -115,7 +101,7 @@
 
 fun print_pred_mode_table string_of_entry pred_mode_table =
   let
-    fun print_mode pred ((pol, mode), entry) =  "mode : " ^ string_of_mode mode
+    fun print_mode pred ((_, mode), entry) =  "mode : " ^ string_of_mode mode
       ^ string_of_entry pred mode entry
     fun print_pred (pred, modes) =
       "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
@@ -133,7 +119,7 @@
     fun print pred () = let
       val _ = writeln ("predicate: " ^ pred)
       val _ = writeln ("introrules: ")
-      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm ctxt thm))
+      val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm))
         (rev (intros_of ctxt pred)) ()
     in
       if (has_elim ctxt pred) then
@@ -159,7 +145,7 @@
 
 (* validity checks *)
 
-fun check_expected_modes options preds modes =
+fun check_expected_modes options _ modes =
   case expected_modes options of
     SOME (s, ms) => (case AList.lookup (op =) modes s of
       SOME modes =>
@@ -200,16 +186,16 @@
 
 fun check_matches_type ctxt predname T ms =
   let
-    fun check (m as Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
-      | check m (T as Type("fun", _)) = (m = Input orelse m = Output)
+    fun check (Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
+      | check m (Type("fun", _)) = (m = Input orelse m = Output)
       | check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
           check m1 T1 andalso check m2 T2 
-      | check Input T = true
-      | check Output T = true
+      | check Input _ = true
+      | check Output _ = true
       | check Bool @{typ bool} = true
       | check _ _ = false
     fun check_consistent_modes ms =
-      if forall (fn Fun (m1', m2') => true | _ => false) ms then
+      if forall (fn Fun _ => true | _ => false) ms then
         pairself check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms))
         |> (fn (res1, res2) => res1 andalso res2) 
       else if forall (fn Input => true | Output => true | Pair _ => true | _ => false) ms then
@@ -320,7 +306,7 @@
         $ compilation
     end,
   transform_additional_arguments =
-    fn prem => fn additional_arguments =>
+    fn _ => fn additional_arguments =>
     let
       val [depth] = additional_arguments
       val depth' =
@@ -378,7 +364,7 @@
         Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
     end),
   wrap_compilation =
-  fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
+  fn compfuns => fn _ => fn T => fn mode => fn additional_arguments => fn compilation =>
     let
       val depth = hd (additional_arguments)
       val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
@@ -391,7 +377,7 @@
         $ compilation
     end,
   transform_additional_arguments =
-    fn prem => fn additional_arguments =>
+    fn _ => fn additional_arguments =>
     let
       val [depth, nrandom, size, seed] = additional_arguments
       val depth' =
@@ -413,21 +399,6 @@
   transform_additional_arguments = K I : (indprem -> term list -> term list)
   }
 
-val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {
-  compilation = Annotated,
-  function_name_prefix = "annotated_",
-  compfuns = Predicate_Comp_Funs.compfuns,
-  mk_random = (fn _ => error "no random generation"),
-  modify_funT = I,
-  additional_arguments = K [],
-  wrap_compilation =
-    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
-      mk_tracing ("calling predicate " ^ s ^
-        " with mode " ^ string_of_mode mode) compilation,
-  transform_additional_arguments = K I : (indprem -> term list -> term list)
-  }
-
 val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   {
   compilation = DSeq,
@@ -446,7 +417,7 @@
   compilation = Pos_Random_DSeq,
   function_name_prefix = "random_dseq_",
   compfuns = Random_Sequence_CompFuns.compfuns,
-  mk_random = (fn T => fn additional_arguments =>
+  mk_random = (fn T => fn _ =>
   let
     val random = Const ("Quickcheck.random_class.random",
       @{typ code_numeral} --> @{typ Random.seed} -->
@@ -483,7 +454,7 @@
   compilation = New_Pos_Random_DSeq,
   function_name_prefix = "new_random_dseq_",
   compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns,
-  mk_random = (fn T => fn additional_arguments =>
+  mk_random = (fn T => fn _ =>
   let
     val random = Const ("Quickcheck.random_class.random",
       @{typ code_numeral} --> @{typ Random.seed} -->
@@ -519,7 +490,7 @@
   function_name_prefix = "generator_dseq_",
   compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns,
   mk_random =
-    (fn T => fn additional_arguments =>
+    (fn T => fn _ =>
       Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
         @{typ "Code_Numeral.code_numeral"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T]))),
   modify_funT = I,
@@ -548,7 +519,7 @@
   function_name_prefix = "generator_cps_pos_",
   compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns,
   mk_random =
-    (fn T => fn additional_arguments =>
+    (fn T => fn _ =>
        Const (@{const_name "Quickcheck_Exhaustive.exhaustive"},
        (T --> @{typ "(bool * term list) option"}) -->
          @{typ "code_numeral => (bool * term list) option"})),
@@ -582,7 +553,7 @@
     | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
     | Pos_Generator_CPS => neg_generator_cps_comp_modifiers
     | Neg_Generator_CPS => pos_generator_cps_comp_modifiers
-    | c => comp_modifiers)
+    | _ => comp_modifiers)
 
 (* term construction *)
 
@@ -606,7 +577,7 @@
 
 
 (** specific rpred functions -- move them to the correct place in this file *)
-fun mk_Eval_of (P as (Free (f, _)), T) mode =
+fun mk_Eval_of (P as (Free _), T) mode =
   let
     fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
           let
@@ -615,7 +586,7 @@
           in
             (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
           end
-      | mk_bounds T i = (Bound i, i + 1)
+      | mk_bounds _ i = (Bound i, i + 1)
     fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
     fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
       | mk_tuple tTs = foldr1 mk_prod tTs
@@ -625,13 +596,13 @@
       | mk_split_abs T t = absdummy T t
     val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
     val (inargs, outargs) = split_mode mode args
-    val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
+    val (_, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
     val inner_term = Predicate_Comp_Funs.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
   in
     fold_rev mk_split_abs (binder_types T) inner_term
   end
 
-fun compile_arg compilation_modifiers additional_arguments ctxt param_modes arg = 
+fun compile_arg compilation_modifiers _ _ param_modes arg = 
   let
     fun map_params (t as Free (f, T)) =
       (case (AList.lookup (op =) param_modes f) of
@@ -672,23 +643,13 @@
        (v', mk_empty compfuns U')])
   end;
 
-fun string_of_tderiv ctxt (t, deriv) = 
-  (case (t, deriv) of
-    (t1 $ t2, Mode_App (deriv1, deriv2)) =>
-      string_of_tderiv ctxt (t1, deriv1) ^ " $ " ^ string_of_tderiv ctxt (t2, deriv2)
-  | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
-    "(" ^ string_of_tderiv ctxt (t1, deriv1) ^ ", " ^ string_of_tderiv ctxt (t2, deriv2) ^ ")"
-  | (t, Term Input) => Syntax.string_of_term ctxt t ^ "[Input]"
-  | (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
-  | (t, Context m) => Syntax.string_of_term ctxt t ^ "[" ^ string_of_mode m ^ "]")
-
 fun compile_expr compilation_modifiers ctxt (t, deriv) param_modes additional_arguments =
   let
     val compfuns = Comp_Mod.compfuns compilation_modifiers
     fun expr_of (t, deriv) =
       (case (t, deriv) of
         (t, Term Input) => SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t)
-      | (t, Term Output) => NONE
+      | (_, Term Output) => NONE
       | (Const (name, T), Context mode) =>
         (case alternative_compilation_of ctxt name mode of
           SOME alt_comp => SOME (alt_comp compfuns T)
@@ -698,13 +659,13 @@
             Comp_Mod.funT_of compilation_modifiers mode T)))
       | (Free (s, T), Context m) =>
         (case (AList.lookup (op =) param_modes s) of
-          SOME mode => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
+          SOME _ => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
         | NONE =>
         let
           val bs = map (pair "x") (binder_types (fastype_of t))
           val bounds = map Bound (rev (0 upto (length bs) - 1))
         in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end)
-      | (t, Context m) =>
+      | (t, Context _) =>
         let
           val bs = map (pair "x") (binder_types (fastype_of t))
           val bounds = map Bound (rev (0 upto (length bs) - 1))
@@ -736,7 +697,7 @@
           let
             val (out_ts'', (names', eqs')) =
               fold_map (collect_non_invertible_subterms ctxt) out_ts' (names, []);
-            val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
+            val (out_ts''', (_, constr_vs)) = fold_map distinct_v
               out_ts'' (names', map (rpair []) vs);
             val processed_out_ts = map (compile_arg compilation_modifiers additional_arguments
               ctxt param_modes) out_ts
@@ -815,10 +776,10 @@
    (fn (i, Input) => [(i, [])]
    | (_, Output) => []
    | (_, Fun _) => []
-   | (i, m as Pair (m1, m2)) => map (pair i) (input_positions_pair m))
+   | (i, m as Pair _) => map (pair i) (input_positions_pair m))
      (Predicate_Compile_Aux.strip_fun_mode mode))
 
-fun argument_position_pair mode [] = []
+fun argument_position_pair _ [] = []
   | argument_position_pair (Pair (Fun _, m2)) (2 :: is) = argument_position_pair m2 is
   | argument_position_pair (Pair (m1, m2)) (i :: is) =
     (if eq_mode (m1, Output) andalso i = 2 then
@@ -839,7 +800,7 @@
 
 (** switch detection analysis **)
 
-fun find_switch_test ctxt (i, is) (ts, prems) =
+fun find_switch_test ctxt (i, is) (ts, _) =
   let
     val t = nth_pair is (nth ts i)
     val T = fastype_of t
@@ -895,7 +856,7 @@
 
 fun destruct_constructor_pattern (pat, obj) =
   (case strip_comb pat of
-    (f as Free _, []) => cons (pat, obj)
+    (Free _, []) => cons (pat, obj)
   | (Const (c, T), pat_args) =>
     (case strip_comb obj of
       (Const (c', T'), obj_args) =>
@@ -1024,12 +985,6 @@
 
 (* Definition of executable functions and their intro and elim rules *)
 
-fun print_arities arities = tracing ("Arities:\n" ^
-  cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
-    space_implode " -> " (map
-      (fn NONE => "X" | SOME k' => string_of_int k')
-        (ks @ [SOME k]))) arities));
-
 fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
   | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   | strip_split_abs t = t
@@ -1120,7 +1075,7 @@
     ((introthm, elimthm), opt_neg_introthm)
   end
 
-fun create_constname_of_mode options thy prefix name T mode = 
+fun create_constname_of_mode options thy prefix name _ mode = 
   let
     val system_proposal = prefix ^ (Long_Name.base_name name)
       ^ "_" ^ ascii_string_of_mode mode
@@ -1139,7 +1094,7 @@
         val mode_cbasename = Long_Name.base_name mode_cname
         val funT = funT_of compfuns mode T
         val (args, _) = fold_map (mk_args true) ((strip_fun_mode mode) ~~ (binder_types T)) []
-        fun strip_eval m t =
+        fun strip_eval _ t =
           let
             val t' = strip_split_abs t
             val (r, _) = Predicate_Comp_Funs.dest_Eval t'
@@ -1167,7 +1122,7 @@
     thy |> defined_function_of Pred name |> fold create_definition modes
   end;
 
-fun define_functions comp_modifiers compfuns options preds (name, modes) thy =
+fun define_functions comp_modifiers _ options preds (name, modes) thy =
   let
     val T = AList.lookup (op =) preds name |> the
     fun create_definition mode thy =
@@ -1200,7 +1155,7 @@
 
 fun maps_modes preds_modes_table =
   map (fn (pred, modes) =>
-    (pred, map (fn (mode, value) => value) modes)) preds_modes_table
+    (pred, map (fn (_, value) => value) modes)) preds_modes_table
 
 fun compile_preds options comp_modifiers ctxt all_vs param_vs preds moded_clauses =
   map_preds_modes (fn pred => compile_pred options comp_modifiers ctxt all_vs param_vs pred
@@ -1210,21 +1165,21 @@
   map_preds_modes (prove_pred options thy clauses preds)
     (join_preds_modes moded_clauses compiled_terms)
 
-fun prove_by_skip options thy _ _ _ compiled_terms =
+fun prove_by_skip _ thy _ _ _ compiled_terms =
   map_preds_modes
-    (fn pred => fn mode => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
+    (fn _ => fn _ => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
     compiled_terms
 
 (* preparation of introduction rules into special datastructures *)
 fun dest_prem ctxt params t =
   (case strip_comb t of
-    (v as Free _, ts) => if member (op =) params v then Prem t else Sidecond t
+    (v as Free _, _) => if member (op =) params v then Prem t else Sidecond t
   | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem ctxt params t of
       Prem t => Negprem t
     | Negprem _ => error ("Double negation not allowed in premise: " ^
         Syntax.string_of_term ctxt (c $ t)) 
     | Sidecond t => Sidecond (c $ t))
-  | (c as Const (s, _), ts) =>
+  | (Const (s, _), _) =>
     if is_registered ctxt s then Prem t else Sidecond t
   | _ => Sidecond t)
 
@@ -1270,7 +1225,7 @@
     val param_vs = map (fst o dest_Free) params
     fun add_clause intr clauses =
       let
-        val (Const (name, T), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
+        val (Const (name, _), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
         val prems = map (dest_prem ctxt params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
       in
         AList.update op = (name, these (AList.lookup op = clauses name) @
@@ -1479,18 +1434,6 @@
   use_generators = false,
   qname = "depth_limited_equation"})
 
-val add_annotated_equations = gen_add_equations
-  (Steps {
-  define_functions =
-    fn options => fn preds => fn (s, modes) =>
-      define_functions annotated_comp_modifiers Predicate_Comp_Funs.compfuns options preds
-      (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
-  prove = prove_by_skip,
-  add_code_equations = K (K I),
-  comp_modifiers = annotated_comp_modifiers,
-  use_generators = false,
-  qname = "annotated_equation"})
-
 val add_random_equations = gen_add_equations
   (Steps {
   define_functions =
@@ -1668,7 +1611,7 @@
            | New_Pos_Random_DSeq => add_new_random_dseq_equations
            | Pos_Generator_DSeq => add_generator_dseq_equations
            | Pos_Generator_CPS => add_generator_cps_equations
-           | compilation => error ("Compilation not supported")
+           | _ => error ("Compilation not supported")
            ) options [const]))
       end
   in
@@ -1740,7 +1683,7 @@
 
 fun dest_special_compr t =
   let
-    val (inner_t, T_compr) = case t of (Const (@{const_name Collect}, _) $ Abs (x, T, t)) => (t, T)
+    val (inner_t, T_compr) = case t of (Const (@{const_name Collect}, _) $ Abs (_, T, t)) => (t, T)
       | _ => raise TERM ("dest_special_compr", [t])
     val (Ts, conj) = apfst (map snd) (Predicate_Compile_Aux.strip_ex inner_t)
     val [eq, body] = HOLogic.dest_conj conj
@@ -1773,13 +1716,13 @@
 
 (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
 fun analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes
-  (compilation, arguments) t_compr =
+  (compilation, _) t_compr =
   let
     val compfuns = Comp_Mod.compfuns comp_modifiers
     val all_modes_of = all_modes_of compilation
     val (((body, output), T_compr), output_names) =
       case try dest_special_compr t_compr of SOME r => r | NONE => dest_general_compr ctxt t_compr
-    val (pred as Const (name, T), all_args) =
+    val (Const (name, _), all_args) =
       case strip_comb body of
         (Const (name, T), all_args) => (Const (name, T), all_args)
       | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
@@ -1794,7 +1737,7 @@
           case int_ord (length modes1, length modes2) of
             GREATER => error "Not enough mode annotations"
           | LESS => error "Too many mode annotations"
-          | EQUAL => forall (fn (m, NONE) => true | (m, SOME m2) => eq_mode (m, m2))
+          | EQUAL => forall (fn (_, NONE) => true | (m, SOME m2) => eq_mode (m, m2))
             (modes1 ~~ modes2)
         fun mode_instance_of (m1, m2) =
           let
diff -r 94041d602ecb -r 72efd6b4038d src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Nov 12 23:24:40 2012 +0100
@@ -80,13 +80,13 @@
     | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])
 
 (*TODO*)
-fun is_introlike_term t = true
+fun is_introlike_term _ = true
 
 val is_introlike = is_introlike_term o prop_of
 
-fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
+fun check_equation_format_term (t as (Const ("==", _) $ u $ _)) =
   (case strip_comb u of
-    (Const (c, T), args) =>
+    (Const (_, T), args) =>
       if (length (binder_types T) = length args) then
         true
       else
@@ -98,7 +98,7 @@
 val check_equation_format = check_equation_format_term o prop_of
 
 
-fun defining_term_of_equation_term (t as (Const ("==", _) $ u $ v)) = fst (strip_comb u)
+fun defining_term_of_equation_term (Const ("==", _) $ u $ _) = fst (strip_comb u)
   | defining_term_of_equation_term t =
     raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
 
@@ -135,7 +135,7 @@
 fun split_all_pairs thy th =
   let
     val ctxt = Proof_Context.init_global thy
-    val ((_, [th']), ctxt') = Variable.import true [th] ctxt
+    val ((_, [th']), _) = Variable.import true [th] ctxt
     val t = prop_of th'
     val frees = Term.add_frees t [] 
     val freenames = Term.add_free_names t []
@@ -230,7 +230,7 @@
    @{const_name HOL.conj},
    @{const_name HOL.disj}]
 
-fun special_cases (c, T) = member (op =) [
+fun special_cases (c, _) = member (op =) [
   @{const_name Product_Type.Unity},
   @{const_name False},
   @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
@@ -253,18 +253,12 @@
   ] c
 
 
-fun print_specification options thy constname specs = 
-  if show_intermediate_results options then
-    tracing ("Specification of " ^ constname ^ ":\n" ^
-      cat_lines (map (Display.string_of_thm_global thy) specs))
-  else ()
-
 fun obtain_specification_graph options thy t =
   let
     val ctxt = Proof_Context.init_global thy
-    fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
-    fun has_code_pred_intros (c, T) = can (Core_Data.intros_of ctxt) c
-    fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
+    fun is_nondefining_const (c, _) = member (op =) logic_operator_names c
+    fun has_code_pred_intros (c, _) = can (Core_Data.intros_of ctxt) c
+    fun case_consts (c, _) = is_some (Datatype.info_of_case thy c)
     fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
     fun defiants_of specs =
       fold (Term.add_consts o prop_of) specs []
diff -r 94041d602ecb -r 72efd6b4038d src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Nov 12 23:24:40 2012 +0100
@@ -40,7 +40,7 @@
 fun pred_of_function thy name =
   case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
     [] => NONE
-  | [(f, p)] => SOME (fst (dest_Const p))
+  | [(_, p)] => SOME (fst (dest_Const p))
   | _ => error ("Multiple matches possible for lookup of constant " ^ name)
 
 fun defined_const thy name = is_some (pred_of_function thy name)
@@ -78,20 +78,6 @@
   val (func, args) = strip_comb lhs
 in ((func, args), rhs) end;
 
-(* TODO: does not work with higher order functions yet *)
-fun mk_rewr_eq (func, pred) =
-  let
-    val (argTs, resT) = strip_type (fastype_of func)
-    val nctxt =
-      Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
-    val (argnames, nctxt') = fold_map Name.variant (replicate (length argTs) "a") nctxt
-    val (resname, nctxt'') = Name.variant "r" nctxt'
-    val args = map Free (argnames ~~ argTs)
-    val res = Free (resname, resT)
-  in Logic.mk_equals
-      (HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res]))
-  end;
-
 fun folds_map f xs y =
   let
     fun folds_map' acc [] y = [(rev acc, y)]
@@ -126,7 +112,7 @@
                 fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t)
                 val vTs = 
                   fold Term.add_frees inner_prems []
-                  |> filter (fn (x, T) => member (op =) inner_names x)
+                  |> filter (fn (x, _) => member (op =) inner_names x)
                 val t = 
                   fold mk_exists vTs
                   (foldr1 HOLogic.mk_conj (HOLogic.mk_eq (res, resvar) ::
@@ -149,8 +135,8 @@
         else
           error ("unexpected input for flatten or lift" ^ Syntax.string_of_term_global thy t ^
           ", " ^  Syntax.string_of_typ_global thy T)
-    and flatten' (t as Const (name, T)) (names, prems) = [(t, (names, prems))]
-      | flatten' (t as Free (f, T)) (names, prems) = [(t, (names, prems))]
+    and flatten' (t as Const _) (names, prems) = [(t, (names, prems))]
+      | flatten' (t as Free _) (names, prems) = [(t, (names, prems))]
       | flatten' (t as Abs _) (names, prems) = [(t, (names, prems))]
       | flatten' (t as _ $ _) (names, prems) =
       if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then
@@ -182,10 +168,9 @@
         case find_split_thm thy (fst (strip_comb t)) of
           SOME raw_split_thm =>
           let
-            val (f, args) = strip_comb t
             val split_thm = prepare_split_thm (Proof_Context.init_global thy) raw_split_thm
             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 t' = case_betapply thy t
             val subst = Pattern.match thy (split_t, t') (Vartab.empty, Vartab.empty)
             fun flatten_of_assm assm =
@@ -267,7 +252,6 @@
     ([], thy)
   else
     let
-      val consts = map fst specs
       val eqns = maps snd specs
       (* create prednames *)
       val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
@@ -293,10 +277,9 @@
           let
             val names = Term.add_free_names rhs []
           in flatten thy lookup_pred rhs (names, [])
-            |> map (fn (resultt, (names', prems)) =>
+            |> map (fn (resultt, (_, prems)) =>
               Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
           end
-      fun mk_rewr_thm (func, pred) = @{thm refl}
       val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
       val (intrs, thy') = thy
         |> Sign.add_consts_i
diff -r 94041d602ecb -r 72efd6b4038d src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Nov 12 23:24:40 2012 +0100
@@ -19,7 +19,7 @@
 
 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
@@ -37,7 +37,7 @@
       (*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
@@ -156,7 +156,7 @@
         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))
@@ -224,11 +224,6 @@
       (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) =
diff -r 94041d602ecb -r 72efd6b4038d src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Mon Nov 12 23:24:40 2012 +0100
@@ -72,12 +72,12 @@
     val param_derivations = param_derivations_of deriv
     val ho_args = ho_args_of mode args
     val f_tac = case f of
-      Const (name, T) => simp_tac (HOL_basic_ss addsimps 
+      Const (name, _) => simp_tac (HOL_basic_ss addsimps 
          [@{thm eval_pred}, predfun_definition_of ctxt name mode,
          @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
          @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
     | Free _ =>
-      Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
+      Subgoal.FOCUS_PREMS (fn {context, params = params, prems, asms, concl, schematics} =>
         let
           val prems' = maps dest_conjunct_prem (take nargs prems)
         in
@@ -97,7 +97,7 @@
 
 fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
   case strip_comb t of
-    (Const (name, T), args) =>
+    (Const (name, _), args) =>
       let
         val mode = head_mode_of deriv
         val introrule = predfun_intro_of ctxt name mode
@@ -117,7 +117,7 @@
       end
   | (Free _, _) =>
     print_tac options "proving parameter call.."
-    THEN Subgoal.FOCUS_PREMS (fn {context = ctxt, params, prems, asms, concl, schematics} =>
+    THEN Subgoal.FOCUS_PREMS (fn {context, params, prems, asms, concl, schematics} =>
         let
           val param_prem = nth prems premposition
           val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
@@ -136,23 +136,6 @@
 
 fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
 
-fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st
-
-fun check_format ctxt st =
-  let
-    val concl' = Logic.strip_assums_concl (hd (prems_of st))
-    val concl = HOLogic.dest_Trueprop concl'
-    val expr = fst (strip_comb (fst (Predicate_Comp_Funs.dest_Eval concl)))
-    fun valid_expr (Const (@{const_name Predicate.bind}, _)) = true
-      | valid_expr (Const (@{const_name Predicate.single}, _)) = true
-      | valid_expr _ = false
-  in
-    if valid_expr expr then
-      ((*tracing "expression is valid";*) Seq.single st)
-    else
-      ((*tracing "expression is not valid";*) Seq.empty) (* error "check_format: wrong format" *)
-  end
-
 fun prove_match options ctxt nargs out_ts =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -175,7 +158,7 @@
     THEN print_tac options "after prove_match:"
     THEN (DETERM (TRY 
            (rtac eval_if_P 1
-           THEN (SUBPROOF (fn {context = ctxt, params, prems, asms, concl, schematics} =>
+           THEN (SUBPROOF (fn {context, params, prems, asms, concl, schematics} =>
              (REPEAT_DETERM (rtac @{thm conjI} 1
              THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
              THEN print_tac options "if condition to be solved:"
@@ -197,7 +180,7 @@
 fun prove_sidecond ctxt t =
   let
     fun preds_of t nameTs = case strip_comb t of 
-      (f as Const (name, T), args) =>
+      (Const (name, T), args) =>
         if is_registered ctxt name then (name, T) :: nameTs
           else fold preds_of args nameTs
       | _ => nameTs
@@ -221,7 +204,7 @@
       THEN asm_full_simp_tac HOL_basic_ss' 1
       THEN print_tac options "before single intro rule"
       THEN Subgoal.FOCUS_PREMS
-             (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
+             (fn {context, params, prems, asms, concl, schematics} =>
               let
                 val prems' = maps dest_conjunct_prem (take nargs prems)
               in
@@ -267,7 +250,7 @@
               THEN (if (is_some name) then
                   print_tac options "before applying not introduction rule"
                   THEN Subgoal.FOCUS_PREMS
-                    (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
+                    (fn {context, params = params, prems, asms, concl, schematics} =>
                       rtac (the neg_intro_rule) 1
                       THEN rtac (nth prems premposition) 1) ctxt 1
                   THEN print_tac options "after applying not introduction rule"
@@ -364,7 +347,7 @@
     val param_derivations = param_derivations_of deriv
     val ho_args = ho_args_of mode args
     val f_tac = case f of
-        Const (name, T) => full_simp_tac (HOL_basic_ss addsimps 
+        Const (name, _) => full_simp_tac (HOL_basic_ss addsimps 
            (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
            :: @{thm "Product_Type.split_conv"}::[])) 1
       | Free _ => all_tac
@@ -378,7 +361,7 @@
 
 fun prove_expr2 options ctxt (t, deriv) = 
   (case strip_comb t of
-      (Const (name, T), args) =>
+      (Const (name, _), args) =>
         let
           val mode = head_mode_of deriv
           val param_derivations = param_derivations_of deriv
@@ -396,7 +379,7 @@
 
 fun prove_sidecond2 options ctxt t = let
   fun preds_of t nameTs = case strip_comb t of 
-    (f as Const (name, T), args) =>
+    (Const (name, T), args) =>
       if is_registered ctxt name then (name, T) :: nameTs
         else fold preds_of args nameTs
     | _ => nameTs
@@ -415,7 +398,7 @@
 fun prove_clause2 options ctxt pred mode (ts, ps) i =
   let
     val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
-    val (in_ts, clause_out_ts) = split_mode mode ts;
+    val (in_ts, _) = split_mode mode ts;
     val split_ss = HOL_basic_ss' addsimps [@{thm split_eta}, @{thm split_beta},
       @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
     fun prove_prems2 out_ts [] =
@@ -506,7 +489,7 @@
 
 (** proof procedure **)
 
-fun prove_pred options thy clauses preds pred (pol, mode) (moded_clauses, compiled_term) =
+fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) =
   let
     val ctxt = Proof_Context.init_global thy
     val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
diff -r 94041d602ecb -r 72efd6b4038d src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon Nov 12 23:24:40 2012 +0100
@@ -26,15 +26,9 @@
 fun specialisation_of thy atom =
   Item_Net.retrieve (Specialisations.get thy) atom
 
-fun print_specialisations thy =
-  tracing (cat_lines (map (fn (t, spec_t) =>
-      Syntax.string_of_term_global thy t ^ " ~~~> " ^ Syntax.string_of_term_global thy spec_t)
-    (Item_Net.content (Specialisations.get thy))))
-
-fun import (pred, intros) args ctxt =
+fun import (_, intros) args ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val ((Tinst, intros'), ctxt') = Variable.importT intros ctxt
+    val ((_, intros'), ctxt') = Variable.importT intros ctxt
     val pred' = fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intros')))))
     val Ts = binder_types (fastype_of pred')
     val argTs = map fastype_of args
@@ -68,7 +62,6 @@
     val maxidx = fold (Term.maxidx_term o prop_of) intros ~1
     val pats = map (Logic.incr_indexes ([],  maxidx + 1)) pats
     val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
-    val intros_t = map prop_of intros
     val result_pats = map Var (fold_rev Term.add_vars pats [])
     fun mk_fresh_name names =
       let
@@ -85,9 +78,6 @@
     val constname = mk_fresh_name []
     val constT = map fastype_of result_pats ---> @{typ bool}
     val specialised_const = Const (constname, constT)
-    val specialisation =
-      [(HOLogic.mk_Trueprop (list_comb (pred, pats)),
-        HOLogic.mk_Trueprop (list_comb (specialised_const, result_pats)))]
     fun specialise_intro intro =
       (let
         val (prems, concl) = Logic.strip_horn (prop_of intro)
@@ -141,7 +131,7 @@
       end
       | restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names =
         replace_term_and_restrict thy T t Tts free_names
-      | restrict_pattern' thy ((T as Type (Tcon, Ts), t) :: Tts) free_names =
+      | restrict_pattern' thy ((T as Type (Tcon, _), t) :: Tts) free_names =
         case Datatype.get_constrs thy Tcon of
           NONE => replace_term_and_restrict thy T t Tts free_names
         | SOME constrs => (case strip_comb t of
@@ -169,7 +159,6 @@
         (pred as Const (pred_name, _), args) =>
           let
           val Ts = binder_types (Sign.the_const_type thy pred_name)
-          val vnames = map fst (fold Term.add_var_names args [])
           val pats = restrict_pattern thy Ts args
         in
           if (exists (is_nontrivial_constrt thy) pats)
@@ -187,7 +176,7 @@
                       | SOME intros =>
                           specialise_intros ((map fst specs) @ (pred_name :: black_list))
                             (pred, intros) pats thy)
-                  | (t, specialised_t) :: _ => thy
+                  | _ :: _ => thy
                 val atom' =
                   case specialisation_of thy' atom of
                     [] => atom