eliminated dead code and some unused bindings, reported by polyml
authorkrauss
Mon Nov 23 15:05:59 2009 +0100 (2009-11-23)
changeset 33855cd8acf137c9c
parent 33854 26a4cb3a7eae
child 33856 14a658faadb6
eliminated dead code and some unused bindings, reported by polyml
src/HOL/Tools/Function/decompose.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/pattern_split.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Function/scnp_solve.ML
src/HOL/Tools/Function/termination.ML
     1.1 --- a/src/HOL/Tools/Function/decompose.ML	Mon Nov 23 13:45:16 2009 +0100
     1.2 +++ b/src/HOL/Tools/Function/decompose.ML	Mon Nov 23 15:05:59 2009 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4       | _ => no_tac)
     1.5    | _ => no_tac)
     1.6  
     1.7 -fun decompose_tac' ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
     1.8 +fun decompose_tac' cont err_cont D = Termination.CALLS (fn (cs, i) =>
     1.9      let
    1.10        val G = mk_dgraph D cs
    1.11        val sccs = TermGraph.strong_conn G
    1.12 @@ -94,12 +94,7 @@
    1.13  
    1.14  fun decompose_tac ctxt chain_tac cont err_cont =
    1.15      derive_chains ctxt chain_tac
    1.16 -    (decompose_tac' ctxt cont err_cont)
    1.17 -
    1.18 -fun auto_decompose_tac ctxt =
    1.19 -    Termination.TERMINATION ctxt
    1.20 -      (decompose_tac ctxt (auto_tac (clasimpset_of ctxt))
    1.21 -                     (K (K all_tac)) (K (K no_tac)))
    1.22 +    (decompose_tac' cont err_cont)
    1.23  
    1.24  
    1.25  end
     2.1 --- a/src/HOL/Tools/Function/fun.ML	Mon Nov 23 13:45:16 2009 +0100
     2.2 +++ b/src/HOL/Tools/Function/fun.ML	Mon Nov 23 15:05:59 2009 +0100
     2.3 @@ -44,7 +44,7 @@
     2.4               ())
     2.5            end
     2.6            
     2.7 -      val (fname, qs, gs, args, rhs) = split_def ctxt geq 
     2.8 +      val (_, qs, gs, args, _) = split_def ctxt geq 
     2.9                                         
    2.10        val _ = if not (null gs) then err "Conditional equations" else ()
    2.11        val _ = map check_constr_pattern args
     3.1 --- a/src/HOL/Tools/Function/function_core.ML	Mon Nov 23 13:45:16 2009 +0100
     3.2 +++ b/src/HOL/Tools/Function/function_core.ML	Mon Nov 23 15:05:59 2009 +0100
     3.3 @@ -97,8 +97,6 @@
     3.4  
     3.5  
     3.6  (* Theory dependencies. *)
     3.7 -val Pair_inject = @{thm Product_Type.Pair_inject};
     3.8 -
     3.9  val acc_induct_rule = @{thm accp_induct_rule};
    3.10  
    3.11  val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
    3.12 @@ -199,7 +197,7 @@
    3.13  
    3.14  fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
    3.15      let
    3.16 -        val Globals {h, fvar, x, ...} = globals
    3.17 +        val Globals {h, ...} = globals
    3.18  
    3.19          val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
    3.20          val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
    3.21 @@ -298,7 +296,7 @@
    3.22  (* Generates the replacement lemma in fully quantified form. *)
    3.23  fun mk_replacement_lemma thy h ih_elim clause =
    3.24      let
    3.25 -        val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
    3.26 +        val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
    3.27          local open Conv in
    3.28          val ih_conv = arg1_conv o arg_conv o arg_conv
    3.29          end
    3.30 @@ -321,7 +319,7 @@
    3.31      end
    3.32  
    3.33  
    3.34 -fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
    3.35 +fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj =
    3.36      let
    3.37          val Globals {h, y, x, fvar, ...} = globals
    3.38          val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
    3.39 @@ -355,10 +353,10 @@
    3.40  
    3.41  
    3.42  
    3.43 -fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
    3.44 +fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
    3.45      let
    3.46          val Globals {x, y, ranT, fvar, ...} = globals
    3.47 -        val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
    3.48 +        val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
    3.49          val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
    3.50  
    3.51          val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
    3.52 @@ -372,7 +370,7 @@
    3.53          val P = cterm_of thy (mk_eq (y, rhsC))
    3.54          val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
    3.55  
    3.56 -        val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
    3.57 +        val unique_clauses = map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
    3.58  
    3.59          val uniqueness = G_cases
    3.60                             |> forall_elim (cterm_of thy lhs)
    3.61 @@ -430,7 +428,7 @@
    3.62  
    3.63          val _ = trace_msg (K "Proving cases for unique existence...")
    3.64          val (ex1s, values) =
    3.65 -            split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
    3.66 +            split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
    3.67  
    3.68          val _ = trace_msg (K "Proving: Graph is a function")
    3.69          val graph_is_function = complete
    3.70 @@ -523,7 +521,7 @@
    3.71          ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
    3.72    end
    3.73  
    3.74 -fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
    3.75 +fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
    3.76    let
    3.77      val RT = domT --> domT --> boolT
    3.78      val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
    3.79 @@ -700,8 +698,6 @@
    3.80          |> implies_intr D_dcl
    3.81          |> implies_intr D_subset
    3.82  
    3.83 -  val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
    3.84 -
    3.85    val simple_induct_rule =
    3.86        subset_induct_rule
    3.87          |> forall_intr (cterm_of thy D)
    3.88 @@ -724,7 +720,7 @@
    3.89  fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
    3.90      let
    3.91        val thy = ProofContext.theory_of ctxt
    3.92 -      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
    3.93 +      val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
    3.94                        qglr = (oqs, _, _, _), ...} = clause
    3.95        val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
    3.96                            |> fold_rev (curry Logic.mk_implies) gs
    3.97 @@ -748,8 +744,8 @@
    3.98  
    3.99  fun mk_nest_term_case thy globals R' ihyp clause =
   3.100      let
   3.101 -      val Globals {x, z, ...} = globals
   3.102 -      val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
   3.103 +      val Globals {z, ...} = globals
   3.104 +      val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...},tree,
   3.105                        qglr=(oqs, _, _, _), ...} = clause
   3.106  
   3.107        val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
   3.108 @@ -868,7 +864,7 @@
   3.109  
   3.110        fun mk_trsimp clause psimp =
   3.111            let
   3.112 -            val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
   3.113 +            val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
   3.114              val thy = ProofContext.theory_of ctxt
   3.115              val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
   3.116  
   3.117 @@ -925,7 +921,7 @@
   3.118        val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
   3.119  
   3.120        val ((R, RIntro_thmss, R_elim), lthy) =
   3.121 -          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
   3.122 +          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
   3.123  
   3.124        val (_, lthy) =
   3.125            Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
     4.1 --- a/src/HOL/Tools/Function/function_lib.ML	Mon Nov 23 13:45:16 2009 +0100
     4.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Mon Nov 23 15:05:59 2009 +0100
     4.3 @@ -14,9 +14,6 @@
     4.4  fun fold_option f NONE y = y
     4.5    | fold_option f (SOME x) y = f x y;
     4.6  
     4.7 -fun fold_map_option f NONE y = (NONE, y)
     4.8 -  | fold_map_option f (SOME x) y = apfst SOME (f x y);
     4.9 -
    4.10  (* Ex: "The variable" ^ plural " is" "s are" vs *)
    4.11  fun plural sg pl [x] = sg
    4.12    | plural sg pl _ = pl
    4.13 @@ -53,7 +50,7 @@
    4.14  
    4.15  
    4.16  (* FIXME: similar to Variable.focus *)
    4.17 -fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
    4.18 +fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (n,T,b)) =
    4.19      let
    4.20        val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
    4.21        val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
     5.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Mon Nov 23 13:45:16 2009 +0100
     5.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Mon Nov 23 15:05:59 2009 +0100
     5.3 @@ -75,7 +75,7 @@
     5.4      let
     5.5        fun mk_branch concl =
     5.6            let
     5.7 -            val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
     5.8 +            val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
     5.9              val (P, xs) = strip_comb Pxs
    5.10            in
    5.11              SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
    5.12 @@ -103,7 +103,7 @@
    5.13  
    5.14              fun mk_rcinfo pr =
    5.15                  let
    5.16 -                  val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
    5.17 +                  val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
    5.18                    val (P', rcs) = strip_comb Phyp
    5.19                  in
    5.20                    (bidx P', Gvs, Gas, rcs)
    5.21 @@ -151,7 +151,7 @@
    5.22         |> mk_forall_rename ("P", Pbool)
    5.23      end
    5.24  
    5.25 -fun mk_wf ctxt R (IndScheme {T, ...}) =
    5.26 +fun mk_wf R (IndScheme {T, ...}) =
    5.27      HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
    5.28  
    5.29  fun mk_ineqs R (IndScheme {T, cases, branches}) =
    5.30 @@ -198,8 +198,6 @@
    5.31      end
    5.32  
    5.33  
    5.34 -fun mk_hol_imp a b = HOLogic.imp $ a $ b
    5.35 -
    5.36  fun mk_ind_goal thy branches =
    5.37      let
    5.38        fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
    5.39 @@ -256,7 +254,7 @@
    5.40              val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
    5.41                                              |> split_list
    5.42                             
    5.43 -            fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press =
    5.44 +            fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
    5.45                  let
    5.46                    val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
    5.47                             
    5.48 @@ -364,7 +362,7 @@
    5.49      val ineqss = mk_ineqs R scheme
    5.50                     |> map (map (pairself (assume o cert)))
    5.51      val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
    5.52 -    val wf_thm = mk_wf ctxt R scheme |> cert |> assume
    5.53 +    val wf_thm = mk_wf R scheme |> cert |> assume
    5.54  
    5.55      val (descent, pres) = split_list (flat ineqss)
    5.56      val newgoals = complete @ pres @ wf_thm :: descent 
     6.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 23 13:45:16 2009 +0100
     6.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon Nov 23 15:05:59 2009 +0100
     6.3 @@ -75,10 +75,6 @@
     6.4        fold_rev Logic.all vars (Logic.list_implies (prems, concl))
     6.5      end
     6.6  
     6.7 -fun prove thy solve_tac t =
     6.8 -    cterm_of thy t |> Goal.init
     6.9 -    |> SINGLE solve_tac |> the
    6.10 -
    6.11  fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
    6.12      let
    6.13        val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
    6.14 @@ -137,8 +133,6 @@
    6.15  
    6.16  (** Error reporting **)
    6.17  
    6.18 -fun pr_table table = writeln (cat_lines (map (fn r => implode (map pr_cell r)) table))
    6.19 -
    6.20  fun pr_goals ctxt st =
    6.21      Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
    6.22       |> Pretty.chunks
    6.23 @@ -190,7 +184,7 @@
    6.24  fun lex_order_tac quiet ctxt solve_tac (st: thm) =
    6.25      let
    6.26        val thy = ProofContext.theory_of ctxt
    6.27 -      val ((trueprop $ (wf $ rel)) :: tl) = prems_of st
    6.28 +      val ((_ $ (_ $ rel)) :: tl) = prems_of st
    6.29  
    6.30        val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
    6.31  
     7.1 --- a/src/HOL/Tools/Function/mutual.ML	Mon Nov 23 13:45:16 2009 +0100
     7.2 +++ b/src/HOL/Tools/Function/mutual.ML	Mon Nov 23 15:05:59 2009 +0100
     7.3 @@ -28,8 +28,6 @@
     7.4  
     7.5  type qgar = string * (string * typ) list * term list * term list * term
     7.6  
     7.7 -fun name_of_fqgar ((f, _, _, _, _): qgar) = f
     7.8 -
     7.9  datatype mutual_part =
    7.10    MutualPart of 
    7.11     {
    7.12 @@ -82,7 +80,6 @@
    7.13  fun analyze_eqs ctxt defname fs eqs =
    7.14      let
    7.15        val num = length fs
    7.16 -        val fnames = map fst fs
    7.17          val fqgars = map (split_def ctxt) eqs
    7.18          val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
    7.19                         |> AList.lookup (op =) #> the
    7.20 @@ -108,7 +105,7 @@
    7.21          val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
    7.22          val fsum_var = (fsum_var_name, fsum_type)
    7.23  
    7.24 -        fun define (fvar as (n, T)) caTs resultT i =
    7.25 +        fun define (fvar as (n, _)) caTs resultT i =
    7.26              let
    7.27                  val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
    7.28                  val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 
    7.29 @@ -170,8 +167,8 @@
    7.30        val thy = ProofContext.theory_of ctxt
    7.31                  
    7.32        val oqnames = map fst pre_qs
    7.33 -      val (qs, ctxt') = Variable.variant_fixes oqnames ctxt
    7.34 -                        |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
    7.35 +      val (qs, _) = Variable.variant_fixes oqnames ctxt
    7.36 +        |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
    7.37                          
    7.38        fun inst t = subst_bounds (rev qs, t)
    7.39        val gs = map inst pre_gs
    7.40 @@ -192,7 +189,7 @@
    7.41  
    7.42  fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm -> thm) sum_psimp_eq =
    7.43      let
    7.44 -      val (MutualPart {f=SOME f, f_defthm=SOME f_def, ...}) = get_part fname parts
    7.45 +      val (MutualPart {f=SOME f, ...}) = get_part fname parts
    7.46  
    7.47        val psimp = import sum_psimp_eq
    7.48        val (simp, restore_cond) = case cprems_of psimp of
    7.49 @@ -223,7 +220,7 @@
    7.50      end
    7.51  
    7.52  
    7.53 -fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, RST, parts, ...}) =
    7.54 +fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) =
    7.55      let
    7.56        val cert = cterm_of (ProofContext.theory_of lthy)
    7.57        val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => 
    7.58 @@ -266,8 +263,8 @@
    7.59  fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
    7.60      let
    7.61        val result = inner_cont proof
    7.62 -      val FunctionResult {fs=[f], G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
    7.63 -                        termination,domintros} = result
    7.64 +      val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
    7.65 +        termination, domintros, ...} = result
    7.66                                                                                                                 
    7.67        val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
    7.68                                       (mk_applied_form lthy cargTs (symmetric f_def), f))
     8.1 --- a/src/HOL/Tools/Function/pattern_split.ML	Mon Nov 23 13:45:16 2009 +0100
     8.2 +++ b/src/HOL/Tools/Function/pattern_split.ML	Mon Nov 23 15:05:59 2009 +0100
     8.3 @@ -50,9 +50,6 @@
     8.4  fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
     8.5  fun join_product (xs, ys) = map_product (curry join) xs ys
     8.6  
     8.7 -fun join_list [] = []
     8.8 -  | join_list xs = foldr1 (join_product) xs
     8.9 -
    8.10  
    8.11  exception DISJ
    8.12  
     9.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Mon Nov 23 13:45:16 2009 +0100
     9.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Mon Nov 23 15:05:59 2009 +0100
     9.3 @@ -73,7 +73,7 @@
     9.4  
     9.5  val multiset_setup = Multiset_Setup.put o SOME
     9.6  
     9.7 -fun undef x = error "undef"
     9.8 +fun undef _ = error "undef"
     9.9  fun get_multiset_setup thy = Multiset_Setup.get thy
    9.10    |> the_default (Multiset
    9.11  { msetT = undef, mk_mset=undef,
    9.12 @@ -153,14 +153,13 @@
    9.13  
    9.14  (* Reconstruction *)
    9.15  
    9.16 -fun reconstruct_tac ctxt D cs (gp as GP (_, gs)) certificate =
    9.17 +fun reconstruct_tac ctxt D cs (GP (_, gs)) certificate =
    9.18    let
    9.19      val thy = ProofContext.theory_of ctxt
    9.20      val Multiset
    9.21            { msetT, mk_mset,
    9.22 -            mset_regroup_conv, mset_member_tac,
    9.23 -            mset_nonempty_tac, mset_pwleq_tac, set_of_simps,
    9.24 -            smsI', wmsI2'', wmsI1, reduction_pair=ms_rp } 
    9.25 +            mset_regroup_conv, mset_pwleq_tac, set_of_simps,
    9.26 +            smsI', wmsI2'', wmsI1, reduction_pair=ms_rp, ...} 
    9.27          = get_multiset_setup thy
    9.28  
    9.29      fun measure_fn p = nth (Termination.get_measures D p)
    9.30 @@ -179,7 +178,7 @@
    9.31  
    9.32      fun prove_lev strict g =
    9.33        let
    9.34 -        val G (p, q, el) = nth gs g
    9.35 +        val G (p, q, _) = nth gs g
    9.36  
    9.37          fun less_proof strict (j, b) (i, a) =
    9.38            let
    9.39 @@ -307,11 +306,10 @@
    9.40    | print_cell (SOME (False _)) = "-"
    9.41    | print_cell (NONE) = "?"
    9.42  
    9.43 -fun print_error ctxt D = CALLS (fn (cs, i) =>
    9.44 +fun print_error ctxt D = CALLS (fn (cs, _) =>
    9.45    let
    9.46      val np = get_num_points D
    9.47      val ms = map_range (get_measures D) np
    9.48 -    val tys = map_range (get_types D) np
    9.49      fun index xs = (1 upto length xs) ~~ xs
    9.50      fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
    9.51      val ims = index (map index ms)
    10.1 --- a/src/HOL/Tools/Function/scnp_solve.ML	Mon Nov 23 13:45:16 2009 +0100
    10.2 +++ b/src/HOL/Tools/Function/scnp_solve.ML	Mon Nov 23 15:05:59 2009 +0100
    10.3 @@ -76,7 +76,7 @@
    10.4    Function_Common.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
    10.5  
    10.6  (* "Virtual constructors" for various propositional variables *)
    10.7 -fun var_constrs (gp as GP (arities, gl)) =
    10.8 +fun var_constrs (gp as GP (arities, _)) =
    10.9    let
   10.10      val n = Int.max (num_graphs gp, num_prog_pts gp)
   10.11      val k = fold Integer.max arities 1
    11.1 --- a/src/HOL/Tools/Function/termination.ML	Mon Nov 23 13:45:16 2009 +0100
    11.2 +++ b/src/HOL/Tools/Function/termination.ML	Mon Nov 23 15:05:59 2009 +0100
    11.3 @@ -148,7 +148,7 @@
    11.4      val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
    11.5      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
    11.6        let
    11.7 -        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
    11.8 +        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ _)
    11.9            = Term.strip_qnt_body "Ex" c
   11.10        in cons r o cons l end
   11.11    in
   11.12 @@ -181,7 +181,6 @@
   11.13  
   11.14  fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   11.15    let
   11.16 -    val n = get_num_points D
   11.17      val (sk, _, _, _, _) = D
   11.18      val vs = Term.strip_qnt_vars "Ex" c
   11.19  
   11.20 @@ -196,7 +195,7 @@
   11.21    | dest_call D t = error "dest_call"
   11.22  
   11.23  
   11.24 -fun derive_desc_aux thy tac c (vs, p, l', q, r', Gam) m1 m2 D =
   11.25 +fun derive_desc_aux thy tac c (vs, _, l', _, r', Gam) m1 m2 D =
   11.26    case get_descent D c m1 m2 of
   11.27      SOME _ => D
   11.28    | NONE => let
   11.29 @@ -225,7 +224,7 @@
   11.30  
   11.31  (* all descents in one go *)
   11.32  fun derive_descents thy tac c D =
   11.33 -  let val cdesc as (vs, p, l', q, r', Gam) = dest_call D c
   11.34 +  let val cdesc as (_, p, _, q, _, _) = dest_call D c
   11.35    in fold_product (derive_desc_aux thy tac c cdesc)
   11.36         (get_measures D p) (get_measures D q) D
   11.37    end
   11.38 @@ -280,7 +279,7 @@
   11.39      let
   11.40        val thy = ProofContext.theory_of ctxt
   11.41        val cert = cterm_of (theory_of_thm st)
   11.42 -      val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
   11.43 +      val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
   11.44  
   11.45        fun mk_compr ineq =
   11.46            let