dropped dead code
authorhaftmann
Mon Nov 12 23:24:40 2012 +0100 (2012-11-12)
changeset 5005672efd6b4038d
parent 50055 94041d602ecb
child 50057 57209cfbf16b
dropped dead code
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/mode_inference.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Mon Nov 12 23:24:40 2012 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Mon Nov 12 23:24:40 2012 +0100
     1.3 @@ -212,8 +212,7 @@
     1.4      fun PEEK f dependent_tactic st = dependent_tactic (f st) st
     1.5      fun meta_eq_of th = th RS @{thm eq_reflection}
     1.6      val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
     1.7 -    fun instantiate i n {context = ctxt, params = p, prems = prems,
     1.8 -      asms = a, concl = cl, schematics = s}  =
     1.9 +    fun instantiate i n {context, params, prems, asms, concl, schematics} =
    1.10        let
    1.11          fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
    1.12          fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
    1.13 @@ -293,10 +292,10 @@
    1.14  
    1.15  fun add_intro (opt_case_name, thm) thy =
    1.16    let
    1.17 -    val (name, T) = dest_Const (fst (strip_intro_concl thm))
    1.18 +    val (name, _) = dest_Const (fst (strip_intro_concl thm))
    1.19      fun cons_intro gr =
    1.20       case try (Graph.get_node gr) name of
    1.21 -       SOME pred_data => Graph.map_node name (map_pred_data
    1.22 +       SOME _ => Graph.map_node name (map_pred_data
    1.23           (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
    1.24       | NONE => Graph.new_node (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr
    1.25    in PredData.map cons_intro thy end
    1.26 @@ -386,9 +385,6 @@
    1.27          val pred = Const (name, Sign.the_const_type thy name)
    1.28          val ctxt = Proof_Context.init_global thy
    1.29          val elim_t = mk_casesrule ctxt pred (map snd named_intros')
    1.30 -        val nparams = (case try (Inductive.the_inductive ctxt) name of
    1.31 -            SOME (_, result) => length (Inductive.params_of (#raw_induct result))
    1.32 -          | NONE => 0)
    1.33          val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
    1.34        in
    1.35          ((named_intros', SOME elim'), true)
    1.36 @@ -417,7 +413,7 @@
    1.37      (* thm refl is a dummy thm *)
    1.38      val modes = map fst compilations
    1.39      val (needs_random, non_random_modes) = pairself (map fst)
    1.40 -      (List.partition (fn (m, (fun_name, random)) => random) compilations)
    1.41 +      (List.partition (fn (_, (_, random)) => random) compilations)
    1.42      val non_random_dummys = map (rpair "dummy") non_random_modes
    1.43      val all_dummys = map (rpair "dummy") modes
    1.44      val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
     2.1 --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Mon Nov 12 23:24:40 2012 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Mon Nov 12 23:24:40 2012 +0100
     2.3 @@ -60,13 +60,6 @@
     2.4  datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
     2.5    | Mode_Pair of mode_derivation * mode_derivation | Term of mode
     2.6  
     2.7 -fun string_of_derivation (Mode_App (m1, m2)) =
     2.8 -  "App (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
     2.9 -  | string_of_derivation (Mode_Pair (m1, m2)) =
    2.10 -  "Pair (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
    2.11 -  | string_of_derivation (Term m) = "Term (" ^ string_of_mode m ^ ")"
    2.12 -  | string_of_derivation (Context m) = "Context (" ^ string_of_mode m ^ ")"
    2.13 -
    2.14  fun strip_mode_derivation deriv =
    2.15    let
    2.16      fun strip (Mode_App (deriv1, deriv2)) ds = strip deriv1 (deriv2 :: ds)
    2.17 @@ -118,43 +111,20 @@
    2.18      (Syntax.string_of_term ctxt t) ^ "(sidecondition)"
    2.19    | string_of_prem ctxt _ = raise Fail "string_of_prem: unexpected input"
    2.20  
    2.21 -fun string_of_clause ctxt pred (ts, prems) =
    2.22 -  (space_implode " --> "
    2.23 -  (map (string_of_prem ctxt) prems)) ^ " --> " ^ pred ^ " "
    2.24 -   ^ (space_implode " " (map (Syntax.string_of_term ctxt) ts))
    2.25 -
    2.26  type mode_analysis_options =
    2.27    {use_generators : bool,
    2.28    reorder_premises : bool,
    2.29    infer_pos_and_neg_modes : bool}
    2.30  
    2.31 -fun is_constrt thy =
    2.32 -  let
    2.33 -    val cnstrs = flat (maps
    2.34 -      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
    2.35 -      (Symtab.dest (Datatype.get_all thy)));
    2.36 -    fun check t = (case strip_comb t of
    2.37 -        (Free _, []) => true
    2.38 -      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
    2.39 -            (SOME (i, Tname), Type (Tname', _)) =>
    2.40 -              length ts = i andalso Tname = Tname' andalso forall check ts
    2.41 -          | _ => false)
    2.42 -      | _ => false)
    2.43 -  in check end;
    2.44 -
    2.45  (*** check if a type is an equality type (i.e. doesn't contain fun)
    2.46    FIXME this is only an approximation ***)
    2.47  fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
    2.48    | is_eqT _ = true;
    2.49  
    2.50 -fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
    2.51 +fun term_vs tm = fold_aterms (fn Free (x, _) => cons x | _ => I) tm [];
    2.52  val terms_vs = distinct (op =) o maps term_vs;
    2.53  
    2.54 -(** collect all Frees in a term (with duplicates!) **)
    2.55 -fun term_vTs tm =
    2.56 -  fold_aterms (fn Free xT => cons xT | _ => I) tm [];
    2.57 -
    2.58 -fun print_failed_mode options thy modes p (pol, m) rs is =
    2.59 +fun print_failed_mode options p (_, m) is =
    2.60    if show_mode_inference options then
    2.61      let
    2.62        val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
    2.63 @@ -162,7 +132,7 @@
    2.64      in () end
    2.65    else ()
    2.66  
    2.67 -fun error_of p (pol, m) is =
    2.68 +fun error_of p (_, m) is =
    2.69    "  Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
    2.70          p ^ " violates mode " ^ string_of_mode m
    2.71  
    2.72 @@ -195,27 +165,10 @@
    2.73      fold find' xs NONE
    2.74    end
    2.75    
    2.76 -fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
    2.77 -val terms_vs = distinct (op =) o maps term_vs;
    2.78 -
    2.79 -fun input_mode T =
    2.80 -  let
    2.81 -    val (Ts, U) = strip_type T
    2.82 -  in
    2.83 -    fold_rev (curry Fun) (map (K Input) Ts) Input
    2.84 -  end
    2.85 -
    2.86 -fun output_mode T =
    2.87 -  let
    2.88 -    val (Ts, U) = strip_type T
    2.89 -  in
    2.90 -    fold_rev (curry Fun) (map (K Output) Ts) Output
    2.91 -  end
    2.92 -
    2.93  fun is_invertible_function ctxt (Const (f, _)) = is_constr ctxt f
    2.94    | is_invertible_function ctxt _ = false
    2.95  
    2.96 -fun non_invertible_subterms ctxt (t as Free _) = []
    2.97 +fun non_invertible_subterms ctxt (Free _) = []
    2.98    | non_invertible_subterms ctxt t = 
    2.99    let
   2.100      val (f, args) = strip_comb t
   2.101 @@ -281,7 +234,7 @@
   2.102    | output_terms (t, Term Output) = [t]
   2.103    | output_terms _ = []
   2.104  
   2.105 -fun lookup_mode modes (Const (s, T)) =
   2.106 +fun lookup_mode modes (Const (s, _)) =
   2.107     (case (AList.lookup (op =) modes s) of
   2.108        SOME ms => SOME (map (fn m => (Context m, [])) ms)
   2.109      | NONE => NONE)
   2.110 @@ -312,7 +265,7 @@
   2.111      end*)
   2.112      (case try (all_derivations_of ctxt modes vs) t  of
   2.113        SOME derivs =>
   2.114 -        filter (fn (d, mvars) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
   2.115 +        filter (fn (d, _) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
   2.116      | NONE => (if is_all_input m then [(Context m, [])] else []))
   2.117    | derivations_of ctxt modes vs t m =
   2.118      if eq_mode (m, Input) then
   2.119 @@ -353,7 +306,7 @@
   2.120      SOME (s, _) =>
   2.121        (case AList.lookup (op =) modes s of
   2.122          SOME ms =>
   2.123 -          (case AList.lookup (op =) (map (fn ((p, m), r) => (m, r)) ms) (head_mode_of deriv) of
   2.124 +          (case AList.lookup (op =) (map (fn ((_, m), r) => (m, r)) ms) (head_mode_of deriv) of
   2.125              SOME r => r
   2.126            | NONE => false)
   2.127        | NONE => false)
   2.128 @@ -370,21 +323,16 @@
   2.129      length (filter contains_output args)
   2.130    end
   2.131  
   2.132 -fun lex_ord ord1 ord2 (x, x') =
   2.133 -  case ord1 (x, x') of
   2.134 -    EQUAL => ord2 (x, x')
   2.135 -  | ord => ord
   2.136 -
   2.137  fun lexl_ord [] (x, x') = EQUAL
   2.138    | lexl_ord (ord :: ords') (x, x') =
   2.139      case ord (x, x') of
   2.140        EQUAL => lexl_ord ords' (x, x')
   2.141      | ord => ord
   2.142  
   2.143 -fun deriv_ord' ctxt pol pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
   2.144 +fun deriv_ord' ctxt _ pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
   2.145    let
   2.146      (* prefer functional modes if it is a function *)
   2.147 -    fun fun_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   2.148 +    fun fun_ord ((t1, deriv1, _), (t2, deriv2, _)) =
   2.149        let
   2.150          fun is_functional t mode =
   2.151            case try (fst o dest_Const o fst o strip_comb) t of
   2.152 @@ -398,20 +346,20 @@
   2.153          | (false, false) => EQUAL
   2.154        end
   2.155      (* prefer modes without requirement for generating random values *)
   2.156 -    fun mvars_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   2.157 +    fun mvars_ord ((_, _, mvars1), (_, _, mvars2)) =
   2.158        int_ord (length mvars1, length mvars2)
   2.159      (* prefer non-random modes *)
   2.160 -    fun random_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   2.161 +    fun random_mode_ord ((t1, deriv1, _), (t2, deriv2, _)) =
   2.162        int_ord (if random_mode_in_deriv modes t1 deriv1 then 1 else 0,
   2.163                 if random_mode_in_deriv modes t2 deriv2 then 1 else 0)
   2.164      (* prefer modes with more input and less output *)
   2.165 -    fun output_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   2.166 +    fun output_mode_ord ((_, deriv1, _), (_, deriv2, _)) =
   2.167        int_ord (number_of_output_positions (head_mode_of deriv1),
   2.168          number_of_output_positions (head_mode_of deriv2))
   2.169      (* prefer recursive calls *)
   2.170      fun is_rec_premise t =
   2.171 -      case fst (strip_comb t) of Const (c, T) => c = pred | _ => false
   2.172 -    fun recursive_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   2.173 +      case fst (strip_comb t) of Const (c, _) => c = pred | _ => false
   2.174 +    fun recursive_ord ((t1, _, _), (t2, deriv2, _)) =
   2.175        int_ord (if is_rec_premise t1 then 0 else 1,
   2.176          if is_rec_premise t2 then 0 else 1)
   2.177      val ord = lexl_ord [mvars_ord, fun_ord, random_mode_ord, output_mode_ord, recursive_ord]
   2.178 @@ -424,10 +372,6 @@
   2.179  fun premise_ord thy pol pred modes ((prem1, a1), (prem2, a2)) =
   2.180    rev_option_ord (deriv_ord' thy pol pred modes (dest_indprem prem1) (dest_indprem prem2)) (a1, a2)
   2.181  
   2.182 -fun print_mode_list modes =
   2.183 -  tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
   2.184 -    commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
   2.185 -
   2.186  fun select_mode_prem (mode_analysis_options : mode_analysis_options) (ctxt : Proof.context) pred
   2.187    pol (modes, (pos_modes, neg_modes)) vs ps =
   2.188    let
   2.189 @@ -435,7 +379,7 @@
   2.190            find_least (deriv_ord ctxt pol pred modes t) (all_derivations_of ctxt pos_modes vs t)
   2.191        | choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
   2.192        | choose_mode_of_prem (Negprem t) = find_least (deriv_ord ctxt (not pol) pred modes t)
   2.193 -          (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
   2.194 +          (filter (fn (d, _) => is_all_input (head_mode_of d))
   2.195               (all_derivations_of ctxt neg_modes vs t))
   2.196        | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: unexpected premise " ^ string_of_prem ctxt p)
   2.197    in
   2.198 @@ -451,17 +395,16 @@
   2.199      val vTs = distinct (op =) (fold Term.add_frees (map dest_indprem ps) (fold Term.add_frees ts []))
   2.200      val modes' = modes @ (param_vs ~~ map (fn x => [((true, x), false), ((false, x), false)]) (ho_arg_modes_of mode))
   2.201      fun retrieve_modes_of_pol pol = map (fn (s, ms) =>
   2.202 -      (s, map_filter (fn ((p, m), r) => if p = pol then SOME m else NONE | _ => NONE) ms))
   2.203 +      (s, map_filter (fn ((p, m), _) => if p = pol then SOME m else NONE | _ => NONE) ms))
   2.204      val (pos_modes', neg_modes') =
   2.205        if #infer_pos_and_neg_modes mode_analysis_options then
   2.206          (retrieve_modes_of_pol pol modes', retrieve_modes_of_pol (not pol) modes')
   2.207        else
   2.208          let
   2.209 -          val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
   2.210 +          val modes = map (fn (s, ms) => (s, map (fn ((_, m), _) => m) ms)) modes'
   2.211          in (modes, modes) end
   2.212      val (in_ts, out_ts) = split_mode mode ts
   2.213      val in_vs = union (op =) param_vs (maps (vars_of_destructable_term ctxt) in_ts)
   2.214 -    val out_vs = terms_vs out_ts
   2.215      fun known_vs_after p vs = (case p of
   2.216          Prem t => union (op =) vs (term_vs t)
   2.217        | Sidecond t => union (op =) vs (term_vs t)
   2.218 @@ -480,7 +423,7 @@
   2.219                  (distinct (op =) missing_vars))
   2.220                  @ acc_ps) true (known_vs_after p vs) (filter_out (equal p) ps)
   2.221            else NONE
   2.222 -        | SOME (p, NONE) => NONE
   2.223 +        | SOME (_, NONE) => NONE
   2.224          | NONE => NONE)
   2.225    in
   2.226      case check_mode_prems [] false in_vs ps of
   2.227 @@ -508,7 +451,7 @@
   2.228      fun split xs =
   2.229        let
   2.230          fun split' [] (ys, zs) = (rev ys, rev zs)
   2.231 -          | split' ((m, Error z) :: xs) (ys, zs) = split' xs (ys, z :: zs)
   2.232 +          | split' ((_, Error z) :: xs) (ys, zs) = split' xs (ys, z :: zs)
   2.233            | split' (((m : bool * mode), Success rnd) :: xs) (ys, zs) = split' xs ((m, rnd) :: ys, zs)
   2.234         in
   2.235           split' xs ([], [])
   2.236 @@ -522,7 +465,7 @@
   2.237          cond_timeit false "aux part of check_mode for one mode" (fn _ => 
   2.238          case find_indices is_none res of
   2.239            [] => Success (exists (fn SOME (_, _, true) => true | _ => false) res)
   2.240 -        | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)))
   2.241 +        | is => (print_failed_mode options p m is; Error (error_of p m is)))
   2.242        end
   2.243      val _ = if show_mode_inference options then
   2.244          tracing ("checking " ^ string_of_int (length ms) ^ " modes ...")
   2.245 @@ -537,9 +480,9 @@
   2.246    let
   2.247      val rs = these (AList.lookup (op =) clauses p)
   2.248    in
   2.249 -    (p, map (fn (m, rnd) =>
   2.250 +    (p, map (fn (m, _) =>
   2.251        (m, map
   2.252 -        ((fn (ts, ps, rnd) => (ts, ps)) o the o
   2.253 +        ((fn (ts, ps, _) => (ts, ps)) o the o
   2.254            check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)) ms)
   2.255    end;
   2.256  
   2.257 @@ -567,18 +510,12 @@
   2.258  fun infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt
   2.259    preds all_modes param_vs clauses =
   2.260    let
   2.261 -    fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
   2.262      fun add_needs_random s (false, m) = ((false, m), false)
   2.263        | add_needs_random s (true, m) = ((true, m), needs_random s m)
   2.264      fun add_polarity_and_random_bit s b ms = map (fn m => add_needs_random s (b, m)) ms
   2.265      val prednames = map fst preds
   2.266      (* extramodes contains all modes of all constants, should we only use the necessary ones
   2.267         - what is the impact on performance? *)
   2.268 -    fun predname_of (Prem t) =
   2.269 -        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
   2.270 -      | predname_of (Negprem t) =
   2.271 -        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
   2.272 -      | predname_of _ = I
   2.273      val relevant_prednames = fold (fn (_, clauses') =>
   2.274        fold (fn (_, ps) => fold Term.add_const_names (map dest_indprem ps)) clauses') clauses []
   2.275        |> filter_out (fn name => member (op =) prednames name)
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Nov 12 23:24:40 2012 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Nov 12 23:24:40 2012 +0100
     3.3 @@ -157,7 +157,7 @@
     3.4          map (apsnd (map fst)) proposed_modes,
     3.5        proposed_names =
     3.6          maps (fn (predname, ms) => (map_filter
     3.7 -          (fn (m, NONE) => NONE | (m, SOME name) => SOME ((predname, m), name))) ms) proposed_modes,
     3.8 +          (fn (_, NONE) => NONE | (m, SOME name) => SOME ((predname, m), name))) ms) proposed_modes,
     3.9        show_steps = chk "show_steps",
    3.10        show_intermediate_results = chk "show_intermediate_results",
    3.11        show_proof_trace = chk "show_proof_trace",
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Nov 12 23:24:40 2012 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Nov 12 23:24:40 2012 +0100
     4.3 @@ -931,7 +931,7 @@
     4.4      let
     4.5        val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
     4.6        val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
     4.7 -      val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
     4.8 +      val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
     4.9        val T' = TFree (tname', HOLogic.typeS)
    4.10        val U = TFree (uname, HOLogic.typeS)
    4.11        val y = Free (yname, U)
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Mon Nov 12 23:24:40 2012 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Mon Nov 12 23:24:40 2012 +0100
     5.3 @@ -89,20 +89,20 @@
     5.4  fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if},
     5.5    HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
     5.6  
     5.7 -fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
     5.8 +fun mk_iterate_upto _ _ = error "not implemented yet"
     5.9  
    5.10  fun mk_not t =
    5.11    let
    5.12      val T = mk_monadT HOLogic.unitT
    5.13    in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end
    5.14  
    5.15 -fun mk_Enum f = error "not implemented"
    5.16 +fun mk_Enum _ = error "not implemented"
    5.17  
    5.18 -fun mk_Eval (f, x) = error "not implemented"
    5.19 +fun mk_Eval _ = error "not implemented"
    5.20  
    5.21 -fun dest_Eval t = error "not implemented"
    5.22 +fun dest_Eval _ = error "not implemented"
    5.23  
    5.24 -fun mk_map T1 T2 tf tp = error "not implemented"
    5.25 +fun mk_map _ _ _ _ = error "not implemented"
    5.26  
    5.27  val compfuns = Predicate_Compile_Aux.CompilationFuns
    5.28      {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
    5.29 @@ -138,7 +138,7 @@
    5.30  fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
    5.31    HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
    5.32  
    5.33 -fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
    5.34 +fun mk_iterate_upto _ _ = error "not implemented yet"
    5.35  
    5.36  fun mk_not t =
    5.37    let
    5.38 @@ -148,13 +148,13 @@
    5.39      val T = mk_monadT HOLogic.unitT
    5.40    in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end
    5.41  
    5.42 -fun mk_Enum f = error "not implemented"
    5.43 +fun mk_Enum _ = error "not implemented"
    5.44  
    5.45 -fun mk_Eval (f, x) = error "not implemented"
    5.46 +fun mk_Eval _ = error "not implemented"
    5.47  
    5.48 -fun dest_Eval t = error "not implemented"
    5.49 +fun dest_Eval _ = error "not implemented"
    5.50  
    5.51 -fun mk_map T1 T2 tf tp = error "not implemented"
    5.52 +fun mk_map _ _ _ _ = error "not implemented"
    5.53  
    5.54  val compfuns = Predicate_Compile_Aux.CompilationFuns
    5.55      {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
    5.56 @@ -193,7 +193,7 @@
    5.57  fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if},
    5.58    HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
    5.59  
    5.60 -fun mk_iterate_upto T (f, from, to) = error "not implemented"
    5.61 +fun mk_iterate_upto _ _ = error "not implemented"
    5.62  
    5.63  fun mk_not t =
    5.64    let
    5.65 @@ -202,13 +202,13 @@
    5.66        --> @{typ "code_numeral => (bool * Code_Evaluation.term list) option"}
    5.67    in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end
    5.68  
    5.69 -fun mk_Enum f = error "not implemented"
    5.70 +fun mk_Enum _ = error "not implemented"
    5.71  
    5.72 -fun mk_Eval (f, x) = error "not implemented"
    5.73 +fun mk_Eval _ = error "not implemented"
    5.74  
    5.75 -fun dest_Eval t = error "not implemented"
    5.76 +fun dest_Eval _ = error "not implemented"
    5.77  
    5.78 -fun mk_map T1 T2 tf tp = error "not implemented"
    5.79 +fun mk_map _ _ _ _  = error "not implemented"
    5.80  
    5.81  val compfuns = Predicate_Compile_Aux.CompilationFuns
    5.82      {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
    5.83 @@ -296,7 +296,7 @@
    5.84  fun mk_if cond = Const (@{const_name DSequence.if_seq},
    5.85    HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
    5.86  
    5.87 -fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
    5.88 +fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
    5.89  
    5.90  fun mk_not t = let val T = mk_dseqT HOLogic.unitT
    5.91    in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
    5.92 @@ -347,7 +347,7 @@
    5.93  fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq},
    5.94    HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
    5.95  
    5.96 -fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
    5.97 +fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
    5.98  
    5.99  fun mk_not t =
   5.100    let
   5.101 @@ -408,7 +408,7 @@
   5.102  fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq},
   5.103    HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
   5.104  
   5.105 -fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
   5.106 +fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
   5.107  
   5.108  fun mk_not t =
   5.109    let
   5.110 @@ -599,7 +599,7 @@
   5.111  fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
   5.112    HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
   5.113  
   5.114 -fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
   5.115 +fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
   5.116  
   5.117  fun mk_not t =
   5.118    let
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Nov 12 23:24:40 2012 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Nov 12 23:24:40 2012 +0100
     6.3 @@ -80,20 +80,6 @@
     6.4              HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
     6.5    in mk_eqs x xs end;
     6.6  
     6.7 -fun mk_scomp (t, u) =
     6.8 -  let
     6.9 -    val T = fastype_of t
    6.10 -    val U = fastype_of u
    6.11 -    val [A] = binder_types T
    6.12 -    val D = body_type U                   
    6.13 -  in 
    6.14 -    Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
    6.15 -  end;
    6.16 -
    6.17 -fun dest_randomT (Type ("fun", [@{typ Random.seed},
    6.18 -  Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
    6.19 -  | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
    6.20 -
    6.21  fun mk_tracing s t =
    6.22    Const(@{const_name Code_Evaluation.tracing},
    6.23      @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
    6.24 @@ -115,7 +101,7 @@
    6.25  
    6.26  fun print_pred_mode_table string_of_entry pred_mode_table =
    6.27    let
    6.28 -    fun print_mode pred ((pol, mode), entry) =  "mode : " ^ string_of_mode mode
    6.29 +    fun print_mode pred ((_, mode), entry) =  "mode : " ^ string_of_mode mode
    6.30        ^ string_of_entry pred mode entry
    6.31      fun print_pred (pred, modes) =
    6.32        "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
    6.33 @@ -133,7 +119,7 @@
    6.34      fun print pred () = let
    6.35        val _ = writeln ("predicate: " ^ pred)
    6.36        val _ = writeln ("introrules: ")
    6.37 -      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm ctxt thm))
    6.38 +      val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm))
    6.39          (rev (intros_of ctxt pred)) ()
    6.40      in
    6.41        if (has_elim ctxt pred) then
    6.42 @@ -159,7 +145,7 @@
    6.43  
    6.44  (* validity checks *)
    6.45  
    6.46 -fun check_expected_modes options preds modes =
    6.47 +fun check_expected_modes options _ modes =
    6.48    case expected_modes options of
    6.49      SOME (s, ms) => (case AList.lookup (op =) modes s of
    6.50        SOME modes =>
    6.51 @@ -200,16 +186,16 @@
    6.52  
    6.53  fun check_matches_type ctxt predname T ms =
    6.54    let
    6.55 -    fun check (m as Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
    6.56 -      | check m (T as Type("fun", _)) = (m = Input orelse m = Output)
    6.57 +    fun check (Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
    6.58 +      | check m (Type("fun", _)) = (m = Input orelse m = Output)
    6.59        | check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
    6.60            check m1 T1 andalso check m2 T2 
    6.61 -      | check Input T = true
    6.62 -      | check Output T = true
    6.63 +      | check Input _ = true
    6.64 +      | check Output _ = true
    6.65        | check Bool @{typ bool} = true
    6.66        | check _ _ = false
    6.67      fun check_consistent_modes ms =
    6.68 -      if forall (fn Fun (m1', m2') => true | _ => false) ms then
    6.69 +      if forall (fn Fun _ => true | _ => false) ms then
    6.70          pairself check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms))
    6.71          |> (fn (res1, res2) => res1 andalso res2) 
    6.72        else if forall (fn Input => true | Output => true | Pair _ => true | _ => false) ms then
    6.73 @@ -320,7 +306,7 @@
    6.74          $ compilation
    6.75      end,
    6.76    transform_additional_arguments =
    6.77 -    fn prem => fn additional_arguments =>
    6.78 +    fn _ => fn additional_arguments =>
    6.79      let
    6.80        val [depth] = additional_arguments
    6.81        val depth' =
    6.82 @@ -378,7 +364,7 @@
    6.83          Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
    6.84      end),
    6.85    wrap_compilation =
    6.86 -  fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
    6.87 +  fn compfuns => fn _ => fn T => fn mode => fn additional_arguments => fn compilation =>
    6.88      let
    6.89        val depth = hd (additional_arguments)
    6.90        val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
    6.91 @@ -391,7 +377,7 @@
    6.92          $ compilation
    6.93      end,
    6.94    transform_additional_arguments =
    6.95 -    fn prem => fn additional_arguments =>
    6.96 +    fn _ => fn additional_arguments =>
    6.97      let
    6.98        val [depth, nrandom, size, seed] = additional_arguments
    6.99        val depth' =
   6.100 @@ -413,21 +399,6 @@
   6.101    transform_additional_arguments = K I : (indprem -> term list -> term list)
   6.102    }
   6.103  
   6.104 -val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
   6.105 -  {
   6.106 -  compilation = Annotated,
   6.107 -  function_name_prefix = "annotated_",
   6.108 -  compfuns = Predicate_Comp_Funs.compfuns,
   6.109 -  mk_random = (fn _ => error "no random generation"),
   6.110 -  modify_funT = I,
   6.111 -  additional_arguments = K [],
   6.112 -  wrap_compilation =
   6.113 -    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
   6.114 -      mk_tracing ("calling predicate " ^ s ^
   6.115 -        " with mode " ^ string_of_mode mode) compilation,
   6.116 -  transform_additional_arguments = K I : (indprem -> term list -> term list)
   6.117 -  }
   6.118 -
   6.119  val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   6.120    {
   6.121    compilation = DSeq,
   6.122 @@ -446,7 +417,7 @@
   6.123    compilation = Pos_Random_DSeq,
   6.124    function_name_prefix = "random_dseq_",
   6.125    compfuns = Random_Sequence_CompFuns.compfuns,
   6.126 -  mk_random = (fn T => fn additional_arguments =>
   6.127 +  mk_random = (fn T => fn _ =>
   6.128    let
   6.129      val random = Const ("Quickcheck.random_class.random",
   6.130        @{typ code_numeral} --> @{typ Random.seed} -->
   6.131 @@ -483,7 +454,7 @@
   6.132    compilation = New_Pos_Random_DSeq,
   6.133    function_name_prefix = "new_random_dseq_",
   6.134    compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns,
   6.135 -  mk_random = (fn T => fn additional_arguments =>
   6.136 +  mk_random = (fn T => fn _ =>
   6.137    let
   6.138      val random = Const ("Quickcheck.random_class.random",
   6.139        @{typ code_numeral} --> @{typ Random.seed} -->
   6.140 @@ -519,7 +490,7 @@
   6.141    function_name_prefix = "generator_dseq_",
   6.142    compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns,
   6.143    mk_random =
   6.144 -    (fn T => fn additional_arguments =>
   6.145 +    (fn T => fn _ =>
   6.146        Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
   6.147          @{typ "Code_Numeral.code_numeral"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T]))),
   6.148    modify_funT = I,
   6.149 @@ -548,7 +519,7 @@
   6.150    function_name_prefix = "generator_cps_pos_",
   6.151    compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns,
   6.152    mk_random =
   6.153 -    (fn T => fn additional_arguments =>
   6.154 +    (fn T => fn _ =>
   6.155         Const (@{const_name "Quickcheck_Exhaustive.exhaustive"},
   6.156         (T --> @{typ "(bool * term list) option"}) -->
   6.157           @{typ "code_numeral => (bool * term list) option"})),
   6.158 @@ -582,7 +553,7 @@
   6.159      | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
   6.160      | Pos_Generator_CPS => neg_generator_cps_comp_modifiers
   6.161      | Neg_Generator_CPS => pos_generator_cps_comp_modifiers
   6.162 -    | c => comp_modifiers)
   6.163 +    | _ => comp_modifiers)
   6.164  
   6.165  (* term construction *)
   6.166  
   6.167 @@ -606,7 +577,7 @@
   6.168  
   6.169  
   6.170  (** specific rpred functions -- move them to the correct place in this file *)
   6.171 -fun mk_Eval_of (P as (Free (f, _)), T) mode =
   6.172 +fun mk_Eval_of (P as (Free _), T) mode =
   6.173    let
   6.174      fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
   6.175            let
   6.176 @@ -615,7 +586,7 @@
   6.177            in
   6.178              (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
   6.179            end
   6.180 -      | mk_bounds T i = (Bound i, i + 1)
   6.181 +      | mk_bounds _ i = (Bound i, i + 1)
   6.182      fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
   6.183      fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
   6.184        | mk_tuple tTs = foldr1 mk_prod tTs
   6.185 @@ -625,13 +596,13 @@
   6.186        | mk_split_abs T t = absdummy T t
   6.187      val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
   6.188      val (inargs, outargs) = split_mode mode args
   6.189 -    val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
   6.190 +    val (_, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
   6.191      val inner_term = Predicate_Comp_Funs.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
   6.192    in
   6.193      fold_rev mk_split_abs (binder_types T) inner_term
   6.194    end
   6.195  
   6.196 -fun compile_arg compilation_modifiers additional_arguments ctxt param_modes arg = 
   6.197 +fun compile_arg compilation_modifiers _ _ param_modes arg = 
   6.198    let
   6.199      fun map_params (t as Free (f, T)) =
   6.200        (case (AList.lookup (op =) param_modes f) of
   6.201 @@ -672,23 +643,13 @@
   6.202         (v', mk_empty compfuns U')])
   6.203    end;
   6.204  
   6.205 -fun string_of_tderiv ctxt (t, deriv) = 
   6.206 -  (case (t, deriv) of
   6.207 -    (t1 $ t2, Mode_App (deriv1, deriv2)) =>
   6.208 -      string_of_tderiv ctxt (t1, deriv1) ^ " $ " ^ string_of_tderiv ctxt (t2, deriv2)
   6.209 -  | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
   6.210 -    "(" ^ string_of_tderiv ctxt (t1, deriv1) ^ ", " ^ string_of_tderiv ctxt (t2, deriv2) ^ ")"
   6.211 -  | (t, Term Input) => Syntax.string_of_term ctxt t ^ "[Input]"
   6.212 -  | (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
   6.213 -  | (t, Context m) => Syntax.string_of_term ctxt t ^ "[" ^ string_of_mode m ^ "]")
   6.214 -
   6.215  fun compile_expr compilation_modifiers ctxt (t, deriv) param_modes additional_arguments =
   6.216    let
   6.217      val compfuns = Comp_Mod.compfuns compilation_modifiers
   6.218      fun expr_of (t, deriv) =
   6.219        (case (t, deriv) of
   6.220          (t, Term Input) => SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t)
   6.221 -      | (t, Term Output) => NONE
   6.222 +      | (_, Term Output) => NONE
   6.223        | (Const (name, T), Context mode) =>
   6.224          (case alternative_compilation_of ctxt name mode of
   6.225            SOME alt_comp => SOME (alt_comp compfuns T)
   6.226 @@ -698,13 +659,13 @@
   6.227              Comp_Mod.funT_of compilation_modifiers mode T)))
   6.228        | (Free (s, T), Context m) =>
   6.229          (case (AList.lookup (op =) param_modes s) of
   6.230 -          SOME mode => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
   6.231 +          SOME _ => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
   6.232          | NONE =>
   6.233          let
   6.234            val bs = map (pair "x") (binder_types (fastype_of t))
   6.235            val bounds = map Bound (rev (0 upto (length bs) - 1))
   6.236          in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end)
   6.237 -      | (t, Context m) =>
   6.238 +      | (t, Context _) =>
   6.239          let
   6.240            val bs = map (pair "x") (binder_types (fastype_of t))
   6.241            val bounds = map Bound (rev (0 upto (length bs) - 1))
   6.242 @@ -736,7 +697,7 @@
   6.243            let
   6.244              val (out_ts'', (names', eqs')) =
   6.245                fold_map (collect_non_invertible_subterms ctxt) out_ts' (names, []);
   6.246 -            val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
   6.247 +            val (out_ts''', (_, constr_vs)) = fold_map distinct_v
   6.248                out_ts'' (names', map (rpair []) vs);
   6.249              val processed_out_ts = map (compile_arg compilation_modifiers additional_arguments
   6.250                ctxt param_modes) out_ts
   6.251 @@ -815,10 +776,10 @@
   6.252     (fn (i, Input) => [(i, [])]
   6.253     | (_, Output) => []
   6.254     | (_, Fun _) => []
   6.255 -   | (i, m as Pair (m1, m2)) => map (pair i) (input_positions_pair m))
   6.256 +   | (i, m as Pair _) => map (pair i) (input_positions_pair m))
   6.257       (Predicate_Compile_Aux.strip_fun_mode mode))
   6.258  
   6.259 -fun argument_position_pair mode [] = []
   6.260 +fun argument_position_pair _ [] = []
   6.261    | argument_position_pair (Pair (Fun _, m2)) (2 :: is) = argument_position_pair m2 is
   6.262    | argument_position_pair (Pair (m1, m2)) (i :: is) =
   6.263      (if eq_mode (m1, Output) andalso i = 2 then
   6.264 @@ -839,7 +800,7 @@
   6.265  
   6.266  (** switch detection analysis **)
   6.267  
   6.268 -fun find_switch_test ctxt (i, is) (ts, prems) =
   6.269 +fun find_switch_test ctxt (i, is) (ts, _) =
   6.270    let
   6.271      val t = nth_pair is (nth ts i)
   6.272      val T = fastype_of t
   6.273 @@ -895,7 +856,7 @@
   6.274  
   6.275  fun destruct_constructor_pattern (pat, obj) =
   6.276    (case strip_comb pat of
   6.277 -    (f as Free _, []) => cons (pat, obj)
   6.278 +    (Free _, []) => cons (pat, obj)
   6.279    | (Const (c, T), pat_args) =>
   6.280      (case strip_comb obj of
   6.281        (Const (c', T'), obj_args) =>
   6.282 @@ -1024,12 +985,6 @@
   6.283  
   6.284  (* Definition of executable functions and their intro and elim rules *)
   6.285  
   6.286 -fun print_arities arities = tracing ("Arities:\n" ^
   6.287 -  cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
   6.288 -    space_implode " -> " (map
   6.289 -      (fn NONE => "X" | SOME k' => string_of_int k')
   6.290 -        (ks @ [SOME k]))) arities));
   6.291 -
   6.292  fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
   6.293    | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   6.294    | strip_split_abs t = t
   6.295 @@ -1120,7 +1075,7 @@
   6.296      ((introthm, elimthm), opt_neg_introthm)
   6.297    end
   6.298  
   6.299 -fun create_constname_of_mode options thy prefix name T mode = 
   6.300 +fun create_constname_of_mode options thy prefix name _ mode = 
   6.301    let
   6.302      val system_proposal = prefix ^ (Long_Name.base_name name)
   6.303        ^ "_" ^ ascii_string_of_mode mode
   6.304 @@ -1139,7 +1094,7 @@
   6.305          val mode_cbasename = Long_Name.base_name mode_cname
   6.306          val funT = funT_of compfuns mode T
   6.307          val (args, _) = fold_map (mk_args true) ((strip_fun_mode mode) ~~ (binder_types T)) []
   6.308 -        fun strip_eval m t =
   6.309 +        fun strip_eval _ t =
   6.310            let
   6.311              val t' = strip_split_abs t
   6.312              val (r, _) = Predicate_Comp_Funs.dest_Eval t'
   6.313 @@ -1167,7 +1122,7 @@
   6.314      thy |> defined_function_of Pred name |> fold create_definition modes
   6.315    end;
   6.316  
   6.317 -fun define_functions comp_modifiers compfuns options preds (name, modes) thy =
   6.318 +fun define_functions comp_modifiers _ options preds (name, modes) thy =
   6.319    let
   6.320      val T = AList.lookup (op =) preds name |> the
   6.321      fun create_definition mode thy =
   6.322 @@ -1200,7 +1155,7 @@
   6.323  
   6.324  fun maps_modes preds_modes_table =
   6.325    map (fn (pred, modes) =>
   6.326 -    (pred, map (fn (mode, value) => value) modes)) preds_modes_table
   6.327 +    (pred, map (fn (_, value) => value) modes)) preds_modes_table
   6.328  
   6.329  fun compile_preds options comp_modifiers ctxt all_vs param_vs preds moded_clauses =
   6.330    map_preds_modes (fn pred => compile_pred options comp_modifiers ctxt all_vs param_vs pred
   6.331 @@ -1210,21 +1165,21 @@
   6.332    map_preds_modes (prove_pred options thy clauses preds)
   6.333      (join_preds_modes moded_clauses compiled_terms)
   6.334  
   6.335 -fun prove_by_skip options thy _ _ _ compiled_terms =
   6.336 +fun prove_by_skip _ thy _ _ _ compiled_terms =
   6.337    map_preds_modes
   6.338 -    (fn pred => fn mode => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
   6.339 +    (fn _ => fn _ => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
   6.340      compiled_terms
   6.341  
   6.342  (* preparation of introduction rules into special datastructures *)
   6.343  fun dest_prem ctxt params t =
   6.344    (case strip_comb t of
   6.345 -    (v as Free _, ts) => if member (op =) params v then Prem t else Sidecond t
   6.346 +    (v as Free _, _) => if member (op =) params v then Prem t else Sidecond t
   6.347    | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem ctxt params t of
   6.348        Prem t => Negprem t
   6.349      | Negprem _ => error ("Double negation not allowed in premise: " ^
   6.350          Syntax.string_of_term ctxt (c $ t)) 
   6.351      | Sidecond t => Sidecond (c $ t))
   6.352 -  | (c as Const (s, _), ts) =>
   6.353 +  | (Const (s, _), _) =>
   6.354      if is_registered ctxt s then Prem t else Sidecond t
   6.355    | _ => Sidecond t)
   6.356  
   6.357 @@ -1270,7 +1225,7 @@
   6.358      val param_vs = map (fst o dest_Free) params
   6.359      fun add_clause intr clauses =
   6.360        let
   6.361 -        val (Const (name, T), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
   6.362 +        val (Const (name, _), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
   6.363          val prems = map (dest_prem ctxt params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
   6.364        in
   6.365          AList.update op = (name, these (AList.lookup op = clauses name) @
   6.366 @@ -1479,18 +1434,6 @@
   6.367    use_generators = false,
   6.368    qname = "depth_limited_equation"})
   6.369  
   6.370 -val add_annotated_equations = gen_add_equations
   6.371 -  (Steps {
   6.372 -  define_functions =
   6.373 -    fn options => fn preds => fn (s, modes) =>
   6.374 -      define_functions annotated_comp_modifiers Predicate_Comp_Funs.compfuns options preds
   6.375 -      (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   6.376 -  prove = prove_by_skip,
   6.377 -  add_code_equations = K (K I),
   6.378 -  comp_modifiers = annotated_comp_modifiers,
   6.379 -  use_generators = false,
   6.380 -  qname = "annotated_equation"})
   6.381 -
   6.382  val add_random_equations = gen_add_equations
   6.383    (Steps {
   6.384    define_functions =
   6.385 @@ -1668,7 +1611,7 @@
   6.386             | New_Pos_Random_DSeq => add_new_random_dseq_equations
   6.387             | Pos_Generator_DSeq => add_generator_dseq_equations
   6.388             | Pos_Generator_CPS => add_generator_cps_equations
   6.389 -           | compilation => error ("Compilation not supported")
   6.390 +           | _ => error ("Compilation not supported")
   6.391             ) options [const]))
   6.392        end
   6.393    in
   6.394 @@ -1740,7 +1683,7 @@
   6.395  
   6.396  fun dest_special_compr t =
   6.397    let
   6.398 -    val (inner_t, T_compr) = case t of (Const (@{const_name Collect}, _) $ Abs (x, T, t)) => (t, T)
   6.399 +    val (inner_t, T_compr) = case t of (Const (@{const_name Collect}, _) $ Abs (_, T, t)) => (t, T)
   6.400        | _ => raise TERM ("dest_special_compr", [t])
   6.401      val (Ts, conj) = apfst (map snd) (Predicate_Compile_Aux.strip_ex inner_t)
   6.402      val [eq, body] = HOLogic.dest_conj conj
   6.403 @@ -1773,13 +1716,13 @@
   6.404  
   6.405  (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
   6.406  fun analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes
   6.407 -  (compilation, arguments) t_compr =
   6.408 +  (compilation, _) t_compr =
   6.409    let
   6.410      val compfuns = Comp_Mod.compfuns comp_modifiers
   6.411      val all_modes_of = all_modes_of compilation
   6.412      val (((body, output), T_compr), output_names) =
   6.413        case try dest_special_compr t_compr of SOME r => r | NONE => dest_general_compr ctxt t_compr
   6.414 -    val (pred as Const (name, T), all_args) =
   6.415 +    val (Const (name, _), all_args) =
   6.416        case strip_comb body of
   6.417          (Const (name, T), all_args) => (Const (name, T), all_args)
   6.418        | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
   6.419 @@ -1794,7 +1737,7 @@
   6.420            case int_ord (length modes1, length modes2) of
   6.421              GREATER => error "Not enough mode annotations"
   6.422            | LESS => error "Too many mode annotations"
   6.423 -          | EQUAL => forall (fn (m, NONE) => true | (m, SOME m2) => eq_mode (m, m2))
   6.424 +          | EQUAL => forall (fn (_, NONE) => true | (m, SOME m2) => eq_mode (m, m2))
   6.425              (modes1 ~~ modes2)
   6.426          fun mode_instance_of (m1, m2) =
   6.427            let
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Nov 12 23:24:40 2012 +0100
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Nov 12 23:24:40 2012 +0100
     7.3 @@ -80,13 +80,13 @@
     7.4      | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])
     7.5  
     7.6  (*TODO*)
     7.7 -fun is_introlike_term t = true
     7.8 +fun is_introlike_term _ = true
     7.9  
    7.10  val is_introlike = is_introlike_term o prop_of
    7.11  
    7.12 -fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
    7.13 +fun check_equation_format_term (t as (Const ("==", _) $ u $ _)) =
    7.14    (case strip_comb u of
    7.15 -    (Const (c, T), args) =>
    7.16 +    (Const (_, T), args) =>
    7.17        if (length (binder_types T) = length args) then
    7.18          true
    7.19        else
    7.20 @@ -98,7 +98,7 @@
    7.21  val check_equation_format = check_equation_format_term o prop_of
    7.22  
    7.23  
    7.24 -fun defining_term_of_equation_term (t as (Const ("==", _) $ u $ v)) = fst (strip_comb u)
    7.25 +fun defining_term_of_equation_term (Const ("==", _) $ u $ _) = fst (strip_comb u)
    7.26    | defining_term_of_equation_term t =
    7.27      raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
    7.28  
    7.29 @@ -135,7 +135,7 @@
    7.30  fun split_all_pairs thy th =
    7.31    let
    7.32      val ctxt = Proof_Context.init_global thy
    7.33 -    val ((_, [th']), ctxt') = Variable.import true [th] ctxt
    7.34 +    val ((_, [th']), _) = Variable.import true [th] ctxt
    7.35      val t = prop_of th'
    7.36      val frees = Term.add_frees t [] 
    7.37      val freenames = Term.add_free_names t []
    7.38 @@ -230,7 +230,7 @@
    7.39     @{const_name HOL.conj},
    7.40     @{const_name HOL.disj}]
    7.41  
    7.42 -fun special_cases (c, T) = member (op =) [
    7.43 +fun special_cases (c, _) = member (op =) [
    7.44    @{const_name Product_Type.Unity},
    7.45    @{const_name False},
    7.46    @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
    7.47 @@ -253,18 +253,12 @@
    7.48    ] c
    7.49  
    7.50  
    7.51 -fun print_specification options thy constname specs = 
    7.52 -  if show_intermediate_results options then
    7.53 -    tracing ("Specification of " ^ constname ^ ":\n" ^
    7.54 -      cat_lines (map (Display.string_of_thm_global thy) specs))
    7.55 -  else ()
    7.56 -
    7.57  fun obtain_specification_graph options thy t =
    7.58    let
    7.59      val ctxt = Proof_Context.init_global thy
    7.60 -    fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
    7.61 -    fun has_code_pred_intros (c, T) = can (Core_Data.intros_of ctxt) c
    7.62 -    fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
    7.63 +    fun is_nondefining_const (c, _) = member (op =) logic_operator_names c
    7.64 +    fun has_code_pred_intros (c, _) = can (Core_Data.intros_of ctxt) c
    7.65 +    fun case_consts (c, _) = is_some (Datatype.info_of_case thy c)
    7.66      fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
    7.67      fun defiants_of specs =
    7.68        fold (Term.add_consts o prop_of) specs []
     8.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Nov 12 23:24:40 2012 +0100
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Nov 12 23:24:40 2012 +0100
     8.3 @@ -40,7 +40,7 @@
     8.4  fun pred_of_function thy name =
     8.5    case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
     8.6      [] => NONE
     8.7 -  | [(f, p)] => SOME (fst (dest_Const p))
     8.8 +  | [(_, p)] => SOME (fst (dest_Const p))
     8.9    | _ => error ("Multiple matches possible for lookup of constant " ^ name)
    8.10  
    8.11  fun defined_const thy name = is_some (pred_of_function thy name)
    8.12 @@ -78,20 +78,6 @@
    8.13    val (func, args) = strip_comb lhs
    8.14  in ((func, args), rhs) end;
    8.15  
    8.16 -(* TODO: does not work with higher order functions yet *)
    8.17 -fun mk_rewr_eq (func, pred) =
    8.18 -  let
    8.19 -    val (argTs, resT) = strip_type (fastype_of func)
    8.20 -    val nctxt =
    8.21 -      Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
    8.22 -    val (argnames, nctxt') = fold_map Name.variant (replicate (length argTs) "a") nctxt
    8.23 -    val (resname, nctxt'') = Name.variant "r" nctxt'
    8.24 -    val args = map Free (argnames ~~ argTs)
    8.25 -    val res = Free (resname, resT)
    8.26 -  in Logic.mk_equals
    8.27 -      (HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res]))
    8.28 -  end;
    8.29 -
    8.30  fun folds_map f xs y =
    8.31    let
    8.32      fun folds_map' acc [] y = [(rev acc, y)]
    8.33 @@ -126,7 +112,7 @@
    8.34                  fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t)
    8.35                  val vTs = 
    8.36                    fold Term.add_frees inner_prems []
    8.37 -                  |> filter (fn (x, T) => member (op =) inner_names x)
    8.38 +                  |> filter (fn (x, _) => member (op =) inner_names x)
    8.39                  val t = 
    8.40                    fold mk_exists vTs
    8.41                    (foldr1 HOLogic.mk_conj (HOLogic.mk_eq (res, resvar) ::
    8.42 @@ -149,8 +135,8 @@
    8.43          else
    8.44            error ("unexpected input for flatten or lift" ^ Syntax.string_of_term_global thy t ^
    8.45            ", " ^  Syntax.string_of_typ_global thy T)
    8.46 -    and flatten' (t as Const (name, T)) (names, prems) = [(t, (names, prems))]
    8.47 -      | flatten' (t as Free (f, T)) (names, prems) = [(t, (names, prems))]
    8.48 +    and flatten' (t as Const _) (names, prems) = [(t, (names, prems))]
    8.49 +      | flatten' (t as Free _) (names, prems) = [(t, (names, prems))]
    8.50        | flatten' (t as Abs _) (names, prems) = [(t, (names, prems))]
    8.51        | flatten' (t as _ $ _) (names, prems) =
    8.52        if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then
    8.53 @@ -182,10 +168,9 @@
    8.54          case find_split_thm thy (fst (strip_comb t)) of
    8.55            SOME raw_split_thm =>
    8.56            let
    8.57 -            val (f, args) = strip_comb t
    8.58              val split_thm = prepare_split_thm (Proof_Context.init_global thy) raw_split_thm
    8.59              val (assms, concl) = Logic.strip_horn (prop_of split_thm)
    8.60 -            val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
    8.61 +            val (_, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
    8.62              val t' = case_betapply thy t
    8.63              val subst = Pattern.match thy (split_t, t') (Vartab.empty, Vartab.empty)
    8.64              fun flatten_of_assm assm =
    8.65 @@ -267,7 +252,6 @@
    8.66      ([], thy)
    8.67    else
    8.68      let
    8.69 -      val consts = map fst specs
    8.70        val eqns = maps snd specs
    8.71        (* create prednames *)
    8.72        val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
    8.73 @@ -293,10 +277,9 @@
    8.74            let
    8.75              val names = Term.add_free_names rhs []
    8.76            in flatten thy lookup_pred rhs (names, [])
    8.77 -            |> map (fn (resultt, (names', prems)) =>
    8.78 +            |> map (fn (resultt, (_, prems)) =>
    8.79                Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
    8.80            end
    8.81 -      fun mk_rewr_thm (func, pred) = @{thm refl}
    8.82        val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
    8.83        val (intrs, thy') = thy
    8.84          |> Sign.add_consts_i
     9.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Nov 12 23:24:40 2012 +0100
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Nov 12 23:24:40 2012 +0100
     9.3 @@ -19,7 +19,7 @@
     9.4  
     9.5  open Predicate_Compile_Aux
     9.6  
     9.7 -fun is_compound ((Const (@{const_name Not}, _)) $ t) =
     9.8 +fun is_compound ((Const (@{const_name Not}, _)) $ _) =
     9.9      error "is_compound: Negation should not occur; preprocessing is defect"
    9.10    | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
    9.11    | is_compound ((Const (@{const_name HOL.disj}, _)) $ _ $ _) = true
    9.12 @@ -37,7 +37,7 @@
    9.13        (*val ((_, [isplit_thm]), _) =
    9.14          Variable.import true [split_thm] (Proof_Context.init_global thy)*)
    9.15        val (assms, concl) = Logic.strip_horn (prop_of split_thm)
    9.16 -      val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
    9.17 +      val (_, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
    9.18        val atom' = case_betapply thy atom
    9.19        val subst = Pattern.match thy (split_t, atom') (Vartab.empty, Vartab.empty)
    9.20        val names' = Term.add_free_names atom' names
    9.21 @@ -156,7 +156,7 @@
    9.22          val nctxt = Name.make_context frees
    9.23          fun mk_introrule t =
    9.24            let
    9.25 -            val ((ps, t'), nctxt') = focus_ex t nctxt
    9.26 +            val ((ps, t'), _) = focus_ex t nctxt
    9.27              val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t')
    9.28            in
    9.29              (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
    9.30 @@ -224,11 +224,6 @@
    9.31        (full_spec, thy'')
    9.32      end;
    9.33  
    9.34 -fun preprocess_term t thy = error "preprocess_pred_term: to implement" 
    9.35 -
    9.36 -fun is_Abs (Abs _) = true
    9.37 -  | is_Abs _       = false
    9.38 -
    9.39  fun flat_higher_order_arguments (intross, thy) =
    9.40    let
    9.41      fun process constname atom (new_defs, thy) =
    10.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Mon Nov 12 23:24:40 2012 +0100
    10.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Mon Nov 12 23:24:40 2012 +0100
    10.3 @@ -72,12 +72,12 @@
    10.4      val param_derivations = param_derivations_of deriv
    10.5      val ho_args = ho_args_of mode args
    10.6      val f_tac = case f of
    10.7 -      Const (name, T) => simp_tac (HOL_basic_ss addsimps 
    10.8 +      Const (name, _) => simp_tac (HOL_basic_ss addsimps 
    10.9           [@{thm eval_pred}, predfun_definition_of ctxt name mode,
   10.10           @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
   10.11           @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
   10.12      | Free _ =>
   10.13 -      Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
   10.14 +      Subgoal.FOCUS_PREMS (fn {context, params = params, prems, asms, concl, schematics} =>
   10.15          let
   10.16            val prems' = maps dest_conjunct_prem (take nargs prems)
   10.17          in
   10.18 @@ -97,7 +97,7 @@
   10.19  
   10.20  fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
   10.21    case strip_comb t of
   10.22 -    (Const (name, T), args) =>
   10.23 +    (Const (name, _), args) =>
   10.24        let
   10.25          val mode = head_mode_of deriv
   10.26          val introrule = predfun_intro_of ctxt name mode
   10.27 @@ -117,7 +117,7 @@
   10.28        end
   10.29    | (Free _, _) =>
   10.30      print_tac options "proving parameter call.."
   10.31 -    THEN Subgoal.FOCUS_PREMS (fn {context = ctxt, params, prems, asms, concl, schematics} =>
   10.32 +    THEN Subgoal.FOCUS_PREMS (fn {context, params, prems, asms, concl, schematics} =>
   10.33          let
   10.34            val param_prem = nth prems premposition
   10.35            val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
   10.36 @@ -136,23 +136,6 @@
   10.37  
   10.38  fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
   10.39  
   10.40 -fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st
   10.41 -
   10.42 -fun check_format ctxt st =
   10.43 -  let
   10.44 -    val concl' = Logic.strip_assums_concl (hd (prems_of st))
   10.45 -    val concl = HOLogic.dest_Trueprop concl'
   10.46 -    val expr = fst (strip_comb (fst (Predicate_Comp_Funs.dest_Eval concl)))
   10.47 -    fun valid_expr (Const (@{const_name Predicate.bind}, _)) = true
   10.48 -      | valid_expr (Const (@{const_name Predicate.single}, _)) = true
   10.49 -      | valid_expr _ = false
   10.50 -  in
   10.51 -    if valid_expr expr then
   10.52 -      ((*tracing "expression is valid";*) Seq.single st)
   10.53 -    else
   10.54 -      ((*tracing "expression is not valid";*) Seq.empty) (* error "check_format: wrong format" *)
   10.55 -  end
   10.56 -
   10.57  fun prove_match options ctxt nargs out_ts =
   10.58    let
   10.59      val thy = Proof_Context.theory_of ctxt
   10.60 @@ -175,7 +158,7 @@
   10.61      THEN print_tac options "after prove_match:"
   10.62      THEN (DETERM (TRY 
   10.63             (rtac eval_if_P 1
   10.64 -           THEN (SUBPROOF (fn {context = ctxt, params, prems, asms, concl, schematics} =>
   10.65 +           THEN (SUBPROOF (fn {context, params, prems, asms, concl, schematics} =>
   10.66               (REPEAT_DETERM (rtac @{thm conjI} 1
   10.67               THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
   10.68               THEN print_tac options "if condition to be solved:"
   10.69 @@ -197,7 +180,7 @@
   10.70  fun prove_sidecond ctxt t =
   10.71    let
   10.72      fun preds_of t nameTs = case strip_comb t of 
   10.73 -      (f as Const (name, T), args) =>
   10.74 +      (Const (name, T), args) =>
   10.75          if is_registered ctxt name then (name, T) :: nameTs
   10.76            else fold preds_of args nameTs
   10.77        | _ => nameTs
   10.78 @@ -221,7 +204,7 @@
   10.79        THEN asm_full_simp_tac HOL_basic_ss' 1
   10.80        THEN print_tac options "before single intro rule"
   10.81        THEN Subgoal.FOCUS_PREMS
   10.82 -             (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
   10.83 +             (fn {context, params, prems, asms, concl, schematics} =>
   10.84                let
   10.85                  val prems' = maps dest_conjunct_prem (take nargs prems)
   10.86                in
   10.87 @@ -267,7 +250,7 @@
   10.88                THEN (if (is_some name) then
   10.89                    print_tac options "before applying not introduction rule"
   10.90                    THEN Subgoal.FOCUS_PREMS
   10.91 -                    (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
   10.92 +                    (fn {context, params = params, prems, asms, concl, schematics} =>
   10.93                        rtac (the neg_intro_rule) 1
   10.94                        THEN rtac (nth prems premposition) 1) ctxt 1
   10.95                    THEN print_tac options "after applying not introduction rule"
   10.96 @@ -364,7 +347,7 @@
   10.97      val param_derivations = param_derivations_of deriv
   10.98      val ho_args = ho_args_of mode args
   10.99      val f_tac = case f of
  10.100 -        Const (name, T) => full_simp_tac (HOL_basic_ss addsimps 
  10.101 +        Const (name, _) => full_simp_tac (HOL_basic_ss addsimps 
  10.102             (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
  10.103             :: @{thm "Product_Type.split_conv"}::[])) 1
  10.104        | Free _ => all_tac
  10.105 @@ -378,7 +361,7 @@
  10.106  
  10.107  fun prove_expr2 options ctxt (t, deriv) = 
  10.108    (case strip_comb t of
  10.109 -      (Const (name, T), args) =>
  10.110 +      (Const (name, _), args) =>
  10.111          let
  10.112            val mode = head_mode_of deriv
  10.113            val param_derivations = param_derivations_of deriv
  10.114 @@ -396,7 +379,7 @@
  10.115  
  10.116  fun prove_sidecond2 options ctxt t = let
  10.117    fun preds_of t nameTs = case strip_comb t of 
  10.118 -    (f as Const (name, T), args) =>
  10.119 +    (Const (name, T), args) =>
  10.120        if is_registered ctxt name then (name, T) :: nameTs
  10.121          else fold preds_of args nameTs
  10.122      | _ => nameTs
  10.123 @@ -415,7 +398,7 @@
  10.124  fun prove_clause2 options ctxt pred mode (ts, ps) i =
  10.125    let
  10.126      val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
  10.127 -    val (in_ts, clause_out_ts) = split_mode mode ts;
  10.128 +    val (in_ts, _) = split_mode mode ts;
  10.129      val split_ss = HOL_basic_ss' addsimps [@{thm split_eta}, @{thm split_beta},
  10.130        @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
  10.131      fun prove_prems2 out_ts [] =
  10.132 @@ -506,7 +489,7 @@
  10.133  
  10.134  (** proof procedure **)
  10.135  
  10.136 -fun prove_pred options thy clauses preds pred (pol, mode) (moded_clauses, compiled_term) =
  10.137 +fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) =
  10.138    let
  10.139      val ctxt = Proof_Context.init_global thy
  10.140      val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon Nov 12 23:24:40 2012 +0100
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon Nov 12 23:24:40 2012 +0100
    11.3 @@ -26,15 +26,9 @@
    11.4  fun specialisation_of thy atom =
    11.5    Item_Net.retrieve (Specialisations.get thy) atom
    11.6  
    11.7 -fun print_specialisations thy =
    11.8 -  tracing (cat_lines (map (fn (t, spec_t) =>
    11.9 -      Syntax.string_of_term_global thy t ^ " ~~~> " ^ Syntax.string_of_term_global thy spec_t)
   11.10 -    (Item_Net.content (Specialisations.get thy))))
   11.11 -
   11.12 -fun import (pred, intros) args ctxt =
   11.13 +fun import (_, intros) args ctxt =
   11.14    let
   11.15 -    val thy = Proof_Context.theory_of ctxt
   11.16 -    val ((Tinst, intros'), ctxt') = Variable.importT intros ctxt
   11.17 +    val ((_, intros'), ctxt') = Variable.importT intros ctxt
   11.18      val pred' = fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intros')))))
   11.19      val Ts = binder_types (fastype_of pred')
   11.20      val argTs = map fastype_of args
   11.21 @@ -68,7 +62,6 @@
   11.22      val maxidx = fold (Term.maxidx_term o prop_of) intros ~1
   11.23      val pats = map (Logic.incr_indexes ([],  maxidx + 1)) pats
   11.24      val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
   11.25 -    val intros_t = map prop_of intros
   11.26      val result_pats = map Var (fold_rev Term.add_vars pats [])
   11.27      fun mk_fresh_name names =
   11.28        let
   11.29 @@ -85,9 +78,6 @@
   11.30      val constname = mk_fresh_name []
   11.31      val constT = map fastype_of result_pats ---> @{typ bool}
   11.32      val specialised_const = Const (constname, constT)
   11.33 -    val specialisation =
   11.34 -      [(HOLogic.mk_Trueprop (list_comb (pred, pats)),
   11.35 -        HOLogic.mk_Trueprop (list_comb (specialised_const, result_pats)))]
   11.36      fun specialise_intro intro =
   11.37        (let
   11.38          val (prems, concl) = Logic.strip_horn (prop_of intro)
   11.39 @@ -141,7 +131,7 @@
   11.40        end
   11.41        | restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names =
   11.42          replace_term_and_restrict thy T t Tts free_names
   11.43 -      | restrict_pattern' thy ((T as Type (Tcon, Ts), t) :: Tts) free_names =
   11.44 +      | restrict_pattern' thy ((T as Type (Tcon, _), t) :: Tts) free_names =
   11.45          case Datatype.get_constrs thy Tcon of
   11.46            NONE => replace_term_and_restrict thy T t Tts free_names
   11.47          | SOME constrs => (case strip_comb t of
   11.48 @@ -169,7 +159,6 @@
   11.49          (pred as Const (pred_name, _), args) =>
   11.50            let
   11.51            val Ts = binder_types (Sign.the_const_type thy pred_name)
   11.52 -          val vnames = map fst (fold Term.add_var_names args [])
   11.53            val pats = restrict_pattern thy Ts args
   11.54          in
   11.55            if (exists (is_nontrivial_constrt thy) pats)
   11.56 @@ -187,7 +176,7 @@
   11.57                        | SOME intros =>
   11.58                            specialise_intros ((map fst specs) @ (pred_name :: black_list))
   11.59                              (pred, intros) pats thy)
   11.60 -                  | (t, specialised_t) :: _ => thy
   11.61 +                  | _ :: _ => thy
   11.62                  val atom' =
   11.63                    case specialisation_of thy' atom of
   11.64                      [] => atom