HOLCF: fix warnings about unreferenced identifiers
authorhuffman
Mon Aug 08 18:36:32 2011 -0700 (2011-08-08)
changeset 4408053d95b52954c
parent 44079 bcc60791b7b9
child 44081 730f7cced3a6
HOLCF: fix warnings about unreferenced identifiers
src/HOL/HOLCF/Tools/Domain/domain.ML
src/HOL/HOLCF/Tools/Domain/domain_axioms.ML
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOL/HOLCF/Tools/cont_proc.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/HOLCF/Tools/holcf_library.ML
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon Aug 08 16:57:37 2011 -0700
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon Aug 08 18:36:32 2011 -0700
     1.3 @@ -35,7 +35,6 @@
     1.4  
     1.5  fun first  (x,_,_) = x
     1.6  fun second (_,x,_) = x
     1.7 -fun third  (_,_,x) = x
     1.8  
     1.9  (* ----- calls for building new thy and thms -------------------------------- *)
    1.10  
    1.11 @@ -78,16 +77,16 @@
    1.12          (binding * (bool * binding option * 'b) list * mixfix) list list =
    1.13          map (fn (_,_,_,cons) => cons) raw_specs
    1.14      val dtnvs' : (string * typ list) list =
    1.15 -        map (fn (dbind, vs, mx) => (Sign.full_name thy dbind, vs)) dtnvs
    1.16 +        map (fn (dbind, vs, _) => (Sign.full_name thy dbind, vs)) dtnvs
    1.17  
    1.18      val all_cons = map (Binding.name_of o first) (flat raw_rhss)
    1.19 -    val test_dupl_cons =
    1.20 +    val _ =
    1.21        case duplicates (op =) all_cons of 
    1.22          [] => false | dups => error ("Duplicate constructors: " 
    1.23                                        ^ commas_quote dups)
    1.24      val all_sels =
    1.25        (map Binding.name_of o map_filter second o maps second) (flat raw_rhss)
    1.26 -    val test_dupl_sels =
    1.27 +    val _ =
    1.28        case duplicates (op =) all_sels of
    1.29          [] => false | dups => error("Duplicate selectors: "^commas_quote dups)
    1.30  
    1.31 @@ -95,7 +94,7 @@
    1.32        case duplicates (op =) (map(fst o dest_TFree)s) of
    1.33          [] => false | dups => error("Duplicate type arguments: " 
    1.34                                      ^commas_quote dups)
    1.35 -    val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs')
    1.36 +    val _ = exists test_dupl_tvars (map snd dtnvs')
    1.37  
    1.38      val sorts : (string * sort) list =
    1.39        let val all_sorts = map (map dest_TFree o snd) dtnvs'
    1.40 @@ -119,7 +118,7 @@
    1.41         non-pcpo-types and invalid use of recursive type
    1.42         replace sorts in type variables on rhs *)
    1.43      val rec_tab = Domain_Take_Proofs.get_rec_tab thy
    1.44 -    fun check_rec no_rec (T as TFree (v,_))  =
    1.45 +    fun check_rec _ (T as TFree (v,_))  =
    1.46          if AList.defined (op =) sorts v then T
    1.47          else error ("Free type variable " ^ quote v ^ " on rhs.")
    1.48        | check_rec no_rec (T as Type (s, Ts)) =
    1.49 @@ -141,7 +140,7 @@
    1.50                    error ("Illegal indirect recursion of type " ^ 
    1.51                           quote (Syntax.string_of_typ_global tmp_thy T) ^
    1.52                           " under type constructor " ^ quote c)))
    1.53 -      | check_rec no_rec (TVar _) = error "extender:check_rec"
    1.54 +      | check_rec _ (TVar _) = error "extender:check_rec"
    1.55  
    1.56      fun prep_arg (lazy, sel, raw_T) =
    1.57        let
    1.58 @@ -154,8 +153,8 @@
    1.59      val rhss : (binding * (bool * binding option * typ) list * mixfix) list list =
    1.60          map prep_rhs raw_rhss
    1.61  
    1.62 -    fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T
    1.63 -    fun mk_con_typ (bind, args, mx) =
    1.64 +    fun mk_arg_typ (lazy, _, T) = if lazy then mk_upT T else T
    1.65 +    fun mk_con_typ (_, args, _) =
    1.66          if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args)
    1.67      fun mk_rhs_typ cons = foldr1 mk_ssumT (map mk_con_typ cons)
    1.68  
    1.69 @@ -174,7 +173,7 @@
    1.70                  Domain_Constructors.add_domain_constructors dbind cons info)
    1.71               (dbinds ~~ rhss ~~ iso_infos)
    1.72  
    1.73 -    val (take_rews, thy) =
    1.74 +    val (_, thy) =
    1.75          Domain_Induction.comp_theorems
    1.76            dbinds take_info constr_infos thy
    1.77    in
    1.78 @@ -184,7 +183,7 @@
    1.79  fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
    1.80    let
    1.81      fun prep (dbind, mx, (lhsT, rhsT)) =
    1.82 -      let val (dname, vs) = dest_Type lhsT
    1.83 +      let val (_, vs) = dest_Type lhsT
    1.84        in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end
    1.85    in
    1.86      Domain_Isomorphism.domain_isomorphism (map prep spec)
     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Mon Aug 08 16:57:37 2011 -0700
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Mon Aug 08 18:36:32 2011 -0700
     2.3 @@ -127,7 +127,7 @@
     2.4            (dbinds ~~ iso_infos) take_info lub_take_thms thy
     2.5  
     2.6      (* define map functions *)
     2.7 -    val (map_info, thy) =
     2.8 +    val (_, thy) =
     2.9          Domain_Isomorphism.define_map_functions
    2.10            (dbinds ~~ iso_infos) thy
    2.11  
     3.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Mon Aug 08 16:57:37 2011 -0700
     3.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Mon Aug 08 18:36:32 2011 -0700
     3.3 @@ -80,9 +80,9 @@
     3.4      fun mk_decl (b, t, mx) = (b, fastype_of t, mx)
     3.5      val decls = map mk_decl specs
     3.6      val thy = Cont_Consts.add_consts decls thy
     3.7 -    fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T)
     3.8 +    fun mk_const (b, T, _) = Const (Sign.full_name thy b, T)
     3.9      val consts = map mk_const decls
    3.10 -    fun mk_def c (b, t, mx) =
    3.11 +    fun mk_def c (b, t, _) =
    3.12        (Binding.suffix_name "_def" b, Logic.mk_equals (c, t))
    3.13      val defs = map2 mk_def consts specs
    3.14      val (def_thms, thy) =
    3.15 @@ -159,7 +159,7 @@
    3.16      val abs_strict = iso_locale RS @{thm iso.abs_strict}
    3.17  
    3.18      (* get types of type isomorphism *)
    3.19 -    val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const)
    3.20 +    val (_, lhsT) = dest_cfunT (fastype_of abs_const)
    3.21  
    3.22      fun vars_of args =
    3.23        let
    3.24 @@ -172,7 +172,7 @@
    3.25      (* define constructor functions *)
    3.26      val ((con_consts, con_defs), thy) =
    3.27        let
    3.28 -        fun one_arg (lazy, T) var = if lazy then mk_up var else var
    3.29 +        fun one_arg (lazy, _) var = if lazy then mk_up var else var
    3.30          fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args))
    3.31          fun mk_abs t = abs_const ` t
    3.32          val rhss = map mk_abs (mk_sinjects (map one_con spec))
    3.33 @@ -187,13 +187,13 @@
    3.34  
    3.35      (* replace bindings with terms in constructor spec *)
    3.36      val spec' : (term * (bool * typ) list) list =
    3.37 -      let fun one_con con (b, args, mx) = (con, args)
    3.38 +      let fun one_con con (_, args, _) = (con, args)
    3.39        in map2 one_con con_consts spec end
    3.40  
    3.41      (* prove exhaustiveness of constructors *)
    3.42      local
    3.43 -      fun arg2typ n (true,  T) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo})))
    3.44 -        | arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo}))
    3.45 +      fun arg2typ n (true,  _) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo})))
    3.46 +        | arg2typ n (false, _) = (n+1, TVar (("'a", n), @{sort pcpo}))
    3.47        fun args2typ n [] = (n, oneT)
    3.48          | args2typ n [arg] = arg2typ n arg
    3.49          | args2typ n (arg::args) =
    3.50 @@ -332,14 +332,14 @@
    3.51          | prime t             = t
    3.52        fun iff_disj (t, []) = mk_not t
    3.53          | iff_disj (t, ts) = mk_eq (t, foldr1 mk_disj ts)
    3.54 -      fun iff_disj2 (t, [], us) = mk_not t
    3.55 -        | iff_disj2 (t, ts, []) = mk_not t
    3.56 +      fun iff_disj2 (t, [], _) = mk_not t
    3.57 +        | iff_disj2 (t, _, []) = mk_not t
    3.58          | iff_disj2 (t, ts, us) =
    3.59            mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us))
    3.60        fun dist_le (con1, args1) (con2, args2) =
    3.61          let
    3.62            val (vs1, zs1) = get_vars args1
    3.63 -          val (vs2, zs2) = get_vars args2 |> pairself (map prime)
    3.64 +          val (vs2, _) = get_vars args2 |> pairself (map prime)
    3.65            val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2))
    3.66            val rhss = map mk_undef zs1
    3.67            val goal = mk_trp (iff_disj (lhs, rhss))
    3.68 @@ -390,7 +390,6 @@
    3.69      (lhsT : typ)
    3.70      (dbind : binding)
    3.71      (con_betas : thm list)
    3.72 -    (exhaust : thm)
    3.73      (iso_locale : thm)
    3.74      (rep_const : term)
    3.75      (thy : theory)
    3.76 @@ -429,7 +428,7 @@
    3.77          | mk_sscases ts = foldr1 mk_sscase ts
    3.78        val body = mk_sscases (map2 one_con fs spec)
    3.79        val rhs = big_lambdas fs (mk_cfcomp (body, rep_const))
    3.80 -      val ((case_consts, case_defs), thy) =
    3.81 +      val ((_, case_defs), thy) =
    3.82            define_consts [(case_bind, rhs, NoSyn)] thy
    3.83        val case_name = Sign.full_name thy case_bind
    3.84      in
    3.85 @@ -457,7 +456,7 @@
    3.86            Library.foldl capp (c_ast authentic con, argvars n args)
    3.87        fun case1 authentic (n, c) =
    3.88            app "_case1" (Ast.strip_positions (con1 authentic n c), expvar n)
    3.89 -      fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
    3.90 +      fun arg1 (n, (_, args)) = List.foldr cabs (expvar n) (argvars n args)
    3.91        fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
    3.92        val case_constant = Ast.Constant (syntax (case_const dummyT))
    3.93        fun case_trans authentic =
    3.94 @@ -541,16 +540,16 @@
    3.95          fun mk_ssnd s = mk_cfcomp (ssnd_const (dest_sprodT (rangeT s)), s)
    3.96          fun mk_down s = mk_cfcomp (from_up (dest_upT (rangeT s)), s)
    3.97  
    3.98 -        fun sels_of_arg s (lazy, NONE,   T) = []
    3.99 -          | sels_of_arg s (lazy, SOME b, T) =
   3.100 +        fun sels_of_arg _ (_, NONE, _) = []
   3.101 +          | sels_of_arg s (lazy, SOME b, _) =
   3.102              [(b, if lazy then mk_down s else s, NoSyn)]
   3.103 -        fun sels_of_args s [] = []
   3.104 +        fun sels_of_args _ [] = []
   3.105            | sels_of_args s (v :: []) = sels_of_arg s v
   3.106            | sels_of_args s (v :: vs) =
   3.107              sels_of_arg (mk_sfst s) v @ sels_of_args (mk_ssnd s) vs
   3.108 -        fun sels_of_cons s [] = []
   3.109 -          | sels_of_cons s ((con, args) :: []) = sels_of_args s args
   3.110 -          | sels_of_cons s ((con, args) :: cs) =
   3.111 +        fun sels_of_cons _ [] = []
   3.112 +          | sels_of_cons s ((_, args) :: []) = sels_of_args s args
   3.113 +          | sels_of_cons s ((_, args) :: cs) =
   3.114              sels_of_args (mk_outl s) args @ sels_of_cons (mk_outr s) cs
   3.115          val sel_eqns : (binding * term * mixfix) list =
   3.116              sels_of_cons rep_const spec
   3.117 @@ -598,7 +597,7 @@
   3.118              val vs : term list = map Free (ns ~~ Ts)
   3.119              val con_app : term = list_ccomb (con, vs)
   3.120              val vs' : (bool * term) list = map #1 args ~~ vs
   3.121 -            fun one_same (n, sel, T) =
   3.122 +            fun one_same (n, sel, _) =
   3.123                let
   3.124                  val xs = map snd (filter_out fst (nth_drop n vs'))
   3.125                  val assms = map (mk_trp o mk_defined) xs
   3.126 @@ -607,7 +606,7 @@
   3.127                in
   3.128                  prove thy defs goal (K tacs)
   3.129                end
   3.130 -            fun one_diff (n, sel, T) =
   3.131 +            fun one_diff (_, sel, T) =
   3.132                let
   3.133                  val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T))
   3.134                in
   3.135 @@ -615,8 +614,8 @@
   3.136                end
   3.137              fun one_con (j, (_, args')) : thm list =
   3.138                let
   3.139 -                fun prep (i, (lazy, NONE, T)) = NONE
   3.140 -                  | prep (i, (lazy, SOME sel, T)) = SOME (i, sel, T)
   3.141 +                fun prep (_, (_, NONE, _)) = NONE
   3.142 +                  | prep (i, (_, SOME sel, T)) = SOME (i, sel, T)
   3.143                  val sels : (int * term * typ) list =
   3.144                    map_filter prep (map_index I args')
   3.145                in
   3.146 @@ -646,12 +645,12 @@
   3.147            in
   3.148              prove thy sel_defs goal (K tacs)
   3.149            end
   3.150 -        fun one_arg (false, SOME sel, T) = SOME (sel_defin sel)
   3.151 +        fun one_arg (false, SOME sel, _) = SOME (sel_defin sel)
   3.152            | one_arg _                    = NONE
   3.153        in
   3.154          case spec2 of
   3.155 -          [(con, args)] => map_filter one_arg args
   3.156 -        | _             => []
   3.157 +          [(_, args)] => map_filter one_arg args
   3.158 +        | _           => []
   3.159        end
   3.160  
   3.161    in
   3.162 @@ -672,19 +671,11 @@
   3.163      (thy : theory) =
   3.164    let
   3.165  
   3.166 -    fun vars_of args =
   3.167 -      let
   3.168 -        val Ts = map snd args
   3.169 -        val ns = Datatype_Prop.make_tnames Ts
   3.170 -      in
   3.171 -        map Free (ns ~~ Ts)
   3.172 -      end
   3.173 -
   3.174      (* define discriminator functions *)
   3.175      local
   3.176 -      fun dis_fun i (j, (con, args)) =
   3.177 +      fun dis_fun i (j, (_, args)) =
   3.178          let
   3.179 -          val (vs, nonlazy) = get_vars args
   3.180 +          val (vs, _) = get_vars args
   3.181            val tr = if i = j then @{term TT} else @{term FF}
   3.182          in
   3.183            big_lambdas vs tr
   3.184 @@ -758,7 +749,6 @@
   3.185      (bindings : binding list)
   3.186      (spec : (term * (bool * typ) list) list)
   3.187      (lhsT : typ)
   3.188 -    (exhaust : thm)
   3.189      (case_const : typ -> term)
   3.190      (case_rews : thm list)
   3.191      (thy : theory) =
   3.192 @@ -776,13 +766,13 @@
   3.193        val x = Free ("x", lhsT)
   3.194        fun k args = Free ("k", map snd args -->> mk_matchT resultT)
   3.195        val fail = mk_fail resultT
   3.196 -      fun mat_fun i (j, (con, args)) =
   3.197 +      fun mat_fun i (j, (_, args)) =
   3.198          let
   3.199 -          val (vs, nonlazy) = get_vars_avoiding ["x","k"] args
   3.200 +          val (vs, _) = get_vars_avoiding ["x","k"] args
   3.201          in
   3.202            if i = j then k args else big_lambdas vs fail
   3.203          end
   3.204 -      fun mat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
   3.205 +      fun mat_eqn (i, (bind, (_, args))) : binding * term * mixfix =
   3.206          let
   3.207            val mat_bind = Binding.prefix_name "match_" bind
   3.208            val funs = map_index (mat_fun i) spec
   3.209 @@ -866,7 +856,6 @@
   3.210      val rep_strict = iso_locale RS @{thm iso.rep_strict}
   3.211      val abs_strict = iso_locale RS @{thm iso.abs_strict}
   3.212      val rep_bottom_iff = iso_locale RS @{thm iso.rep_bottom_iff}
   3.213 -    val abs_bottom_iff = iso_locale RS @{thm iso.abs_bottom_iff}
   3.214      val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict]
   3.215  
   3.216      (* qualify constants and theorems with domain name *)
   3.217 @@ -875,7 +864,7 @@
   3.218      (* define constructor functions *)
   3.219      val (con_result, thy) =
   3.220        let
   3.221 -        fun prep_arg (lazy, sel, T) = (lazy, T)
   3.222 +        fun prep_arg (lazy, _, T) = (lazy, T)
   3.223          fun prep_con (b, args, mx) = (b, map prep_arg args, mx)
   3.224          val con_spec = map prep_con spec
   3.225        in
   3.226 @@ -887,8 +876,8 @@
   3.227      (* prepare constructor spec *)
   3.228      val con_specs : (term * (bool * typ) list) list =
   3.229        let
   3.230 -        fun prep_arg (lazy, sel, T) = (lazy, T)
   3.231 -        fun prep_con c (b, args, mx) = (c, map prep_arg args)
   3.232 +        fun prep_arg (lazy, _, T) = (lazy, T)
   3.233 +        fun prep_con c (_, args, _) = (c, map prep_arg args)
   3.234        in
   3.235          map2 prep_con con_consts spec
   3.236        end
   3.237 @@ -896,13 +885,13 @@
   3.238      (* define case combinator *)
   3.239      val ((case_const : typ -> term, cases : thm list), thy) =
   3.240          add_case_combinator con_specs lhsT dbind
   3.241 -          con_betas exhaust iso_locale rep_const thy
   3.242 +          con_betas iso_locale rep_const thy
   3.243  
   3.244      (* define and prove theorems for selector functions *)
   3.245      val (sel_thms : thm list, thy : theory) =
   3.246        let
   3.247          val sel_spec : (term * (bool * binding option * typ) list) list =
   3.248 -          map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec
   3.249 +          map2 (fn con => fn (_, args, _) => (con, args)) con_consts spec
   3.250        in
   3.251          add_selectors sel_spec rep_const
   3.252            abs_iso_thm rep_strict rep_bottom_iff con_betas thy
   3.253 @@ -916,7 +905,7 @@
   3.254      (* define and prove theorems for match combinators *)
   3.255      val (match_thms : thm list, thy : theory) =
   3.256          add_match_combinators bindings con_specs lhsT
   3.257 -          exhaust case_const cases thy
   3.258 +          case_const cases thy
   3.259  
   3.260      (* restore original signature path *)
   3.261      val thy = Sign.parent_path thy
     4.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Mon Aug 08 16:57:37 2011 -0700
     4.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Mon Aug 08 18:36:32 2011 -0700
     4.3 @@ -221,7 +221,7 @@
     4.4            if length dnames = 1 then ["bottom"] else
     4.5            map (fn s => "bottom_" ^ Long_Name.base_name s) dnames
     4.6        fun one_eq bot (constr_info : Domain_Constructors.constr_info) =
     4.7 -        let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c))
     4.8 +        let fun name_of (c, _) = Long_Name.base_name (fst (dest_Const c))
     4.9          in bot :: map name_of (#con_specs constr_info) end
    4.10      in adms @ flat (map2 one_eq bottoms constr_infos) end
    4.11  
    4.12 @@ -344,7 +344,7 @@
    4.13        val assm1 = mk_trp (list_comb (bisim_const, Rs))
    4.14        val assm2 = mk_trp (R $ x $ y)
    4.15        val goal = mk_trp (mk_eq (x, y))
    4.16 -      fun tacf {prems, context} =
    4.17 +      fun tacf {prems, context = _} =
    4.18          let
    4.19            val rule = hd prems RS coind_lemma
    4.20          in
    4.21 @@ -420,7 +420,7 @@
    4.22  val (take_rewss, thy) =
    4.23      take_theorems dbinds take_info constr_infos thy
    4.24  
    4.25 -val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info
    4.26 +val {take_0_thms, take_strict_thms, ...} = take_info
    4.27  
    4.28  val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss
    4.29  
     5.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Aug 08 16:57:37 2011 -0700
     5.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Aug 08 18:36:32 2011 -0700
     5.3 @@ -86,15 +86,6 @@
     5.4  
     5.5  fun mk_u_defl t = mk_capply (@{const "u_defl"}, t)
     5.6  
     5.7 -fun mk_u_map t =
     5.8 -  let
     5.9 -    val (T, U) = dest_cfunT (fastype_of t)
    5.10 -    val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U)
    5.11 -    val u_map_const = Const (@{const_name u_map}, u_map_type)
    5.12 -  in
    5.13 -    mk_capply (u_map_const, t)
    5.14 -  end
    5.15 -
    5.16  fun emb_const T = Const (@{const_name emb}, T ->> udomT)
    5.17  fun prj_const T = Const (@{const_name prj}, udomT ->> T)
    5.18  fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T)
    5.19 @@ -130,7 +121,7 @@
    5.20  (*************** fixed-point definitions and unfolding theorems ***************)
    5.21  (******************************************************************************)
    5.22  
    5.23 -fun mk_projs []      t = []
    5.24 +fun mk_projs []      _ = []
    5.25    | mk_projs (x::[]) t = [(x, t)]
    5.26    | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t)
    5.27  
    5.28 @@ -187,7 +178,7 @@
    5.29        (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
    5.30        |> Local_Defs.unfold (Proof_Context.init_global thy) @{thms split_conv}
    5.31  
    5.32 -    fun mk_unfold_thms [] thm = []
    5.33 +    fun mk_unfold_thms [] _ = []
    5.34        | mk_unfold_thms (n::[]) thm = [(n, thm)]
    5.35        | mk_unfold_thms (n::ns) thm = let
    5.36            val thmL = thm RS @{thm Pair_eqD1}
    5.37 @@ -271,7 +262,7 @@
    5.38        | mapT T = T ->> T
    5.39  
    5.40      (* declare map functions *)
    5.41 -    fun declare_map_const (tbind, (lhsT, rhsT)) thy =
    5.42 +    fun declare_map_const (tbind, (lhsT, _)) thy =
    5.43        let
    5.44          val map_type = mapT lhsT
    5.45          val map_bind = Binding.suffix_name "_map" tbind
    5.46 @@ -290,7 +281,7 @@
    5.47        val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns)
    5.48        val Ts = (snd o dest_Type o fst o hd) dom_eqns
    5.49        val tab = (Ts ~~ map mapvar Ts) @ tab1
    5.50 -      fun mk_map_spec (((rep_const, abs_const), map_const), (lhsT, rhsT)) =
    5.51 +      fun mk_map_spec (((rep_const, abs_const), _), (lhsT, rhsT)) =
    5.52          let
    5.53            val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT
    5.54            val body = Domain_Take_Proofs.map_of_typ thy tab rhsT
    5.55 @@ -313,7 +304,7 @@
    5.56          fun unprime a = Library.unprefix "'" a
    5.57          fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T)
    5.58          fun mk_assm T = mk_trp (mk_deflation (mk_f T))
    5.59 -        fun mk_goal (map_const, (lhsT, rhsT)) =
    5.60 +        fun mk_goal (map_const, (lhsT, _)) =
    5.61            let
    5.62              val (_, Ts) = dest_Type lhsT
    5.63              val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
    5.64 @@ -343,7 +334,7 @@
    5.65             REPEAT (etac @{thm conjE} 1),
    5.66             REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)])
    5.67        end
    5.68 -    fun conjuncts [] thm = []
    5.69 +    fun conjuncts [] _ = []
    5.70        | conjuncts (n::[]) thm = [(n, thm)]
    5.71        | conjuncts (n::ns) thm = let
    5.72            val thmL = thm RS @{thm conjunct1}
    5.73 @@ -360,7 +351,6 @@
    5.74        fun register_map (dname, args) =
    5.75          Domain_Take_Proofs.add_rec_type (dname, args)
    5.76        val dnames = map (fst o dest_Type o fst) dom_eqns
    5.77 -      val map_names = map (fst o dest_Const) map_consts
    5.78        fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => []
    5.79        val argss = map args dom_eqns
    5.80      in
    5.81 @@ -417,7 +407,7 @@
    5.82      (* this theory is used just for parsing *)
    5.83      val tmp_thy = thy |>
    5.84        Theory.copy |>
    5.85 -      Sign.add_types_global (map (fn (tvs, tbind, mx, _, morphs) =>
    5.86 +      Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) =>
    5.87          (tbind, length tvs, mx)) doms_raw)
    5.88  
    5.89      fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts =
    5.90 @@ -434,28 +424,28 @@
    5.91      (* declare arities in temporary theory *)
    5.92      val tmp_thy =
    5.93        let
    5.94 -        fun arity (vs, tbind, mx, _, _) =
    5.95 +        fun arity (vs, tbind, _, _, _) =
    5.96            (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"})
    5.97        in
    5.98          fold AxClass.axiomatize_arity (map arity doms) tmp_thy
    5.99        end
   5.100  
   5.101      (* check bifiniteness of right-hand sides *)
   5.102 -    fun check_rhs (vs, tbind, mx, rhs, morphs) =
   5.103 +    fun check_rhs (_, _, _, rhs, _) =
   5.104        if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then ()
   5.105        else error ("Type not of sort domain: " ^
   5.106          quote (Syntax.string_of_typ_global tmp_thy rhs))
   5.107      val _ = map check_rhs doms
   5.108  
   5.109      (* domain equations *)
   5.110 -    fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) =
   5.111 +    fun mk_dom_eqn (vs, tbind, _, rhs, _) =
   5.112        let fun arg v = TFree (v, the_sort v)
   5.113        in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end
   5.114      val dom_eqns = map mk_dom_eqn doms
   5.115  
   5.116      (* check for valid type parameters *)
   5.117      val (tyvars, _, _, _, _) = hd doms
   5.118 -    val new_doms = map (fn (tvs, tname, mx, _, _) =>
   5.119 +    val _ = map (fn (tvs, tname, _, _, _) =>
   5.120        let val full_tname = Sign.full_name tmp_thy tname
   5.121        in
   5.122          (case duplicates (op =) tvs of
   5.123 @@ -528,7 +518,7 @@
   5.124      fun make_repdef ((vs, tbind, mx, _, _), defl) thy =
   5.125        let
   5.126          val spec = (tbind, map (rpair dummyS) vs, mx)
   5.127 -        val ((_, _, _, {DEFL, liftemb_def, liftprj_def, ...}), thy) =
   5.128 +        val ((_, _, _, {DEFL, ...}), thy) =
   5.129            Domaindef.add_domaindef false NONE spec defl NONE thy
   5.130          (* declare domain_defl_simps rules *)
   5.131          val thy = Context.theory_map (RepData.add_thm DEFL) thy
   5.132 @@ -557,7 +547,7 @@
   5.133          (DEFL_eq_binds ~~ DEFL_eq_thms)
   5.134  
   5.135      (* define rep/abs functions *)
   5.136 -    fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy =
   5.137 +    fun mk_rep_abs ((tbind, _), (lhsT, rhsT)) thy =
   5.138        let
   5.139          val rep_bind = Binding.suffix_name "_rep" tbind
   5.140          val abs_bind = Binding.suffix_name "_abs" tbind
   5.141 @@ -611,8 +601,7 @@
   5.142      (* definitions and proofs related to map functions *)
   5.143      val (map_info, thy) =
   5.144          define_map_functions (dbinds ~~ iso_infos) thy
   5.145 -    val { map_consts, map_apply_thms, map_unfold_thms,
   5.146 -          map_cont_thm, deflation_map_thms } = map_info
   5.147 +    val { map_consts, map_apply_thms, map_cont_thm, ...} = map_info
   5.148  
   5.149      (* prove isodefl rules for map functions *)
   5.150      val isodefl_thm =
   5.151 @@ -627,7 +616,7 @@
   5.152            | NONE =>
   5.153              let val T = dest_DEFL t
   5.154              in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end
   5.155 -        fun mk_goal (map_const, (T, rhsT)) =
   5.156 +        fun mk_goal (map_const, (T, _)) =
   5.157            let
   5.158              val (_, Ts) = dest_Type T
   5.159              val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
   5.160 @@ -662,7 +651,7 @@
   5.161             REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
   5.162        end
   5.163      val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds
   5.164 -    fun conjuncts [] thm = []
   5.165 +    fun conjuncts [] _ = []
   5.166        | conjuncts (n::[]) thm = [(n, thm)]
   5.167        | conjuncts (n::ns) thm = let
   5.168            val thmL = thm RS @{thm conjunct1}
   5.169 @@ -709,7 +698,7 @@
   5.170        let
   5.171          val lhs = mk_tuple (map mk_lub take_consts)
   5.172          fun is_cpo T = Sign.of_sort thy (T, @{sort cpo})
   5.173 -        fun mk_map_ID (map_const, (lhsT, rhsT)) =
   5.174 +        fun mk_map_ID (map_const, (lhsT, _)) =
   5.175            list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT))))
   5.176          val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns))
   5.177          val goal = mk_trp (mk_eq (lhs, rhs))
   5.178 @@ -736,7 +725,7 @@
   5.179        end
   5.180  
   5.181      (* prove lub of take equals ID *)
   5.182 -    fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
   5.183 +    fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, _)) thy =
   5.184        let
   5.185          val n = Free ("n", natT)
   5.186          val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT)
     6.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Aug 08 16:57:37 2011 -0700
     6.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Aug 08 18:36:32 2011 -0700
     6.3 @@ -159,10 +159,6 @@
     6.4  infix -->>
     6.5  infix 9 `
     6.6  
     6.7 -fun mapT (T as Type (_, Ts)) =
     6.8 -    (map (fn T => T ->> T) Ts) -->> (T ->> T)
     6.9 -  | mapT T = T ->> T
    6.10 -
    6.11  fun mk_deflation t =
    6.12    Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t
    6.13  
    6.14 @@ -227,7 +223,7 @@
    6.15      val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos
    6.16      val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos
    6.17  
    6.18 -    fun mk_projs []      t = []
    6.19 +    fun mk_projs []      _ = []
    6.20        | mk_projs (x::[]) t = [(x, t)]
    6.21        | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t)
    6.22  
    6.23 @@ -239,7 +235,7 @@
    6.24      val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs)
    6.25      val copy_arg = Free ("f", copy_arg_type)
    6.26      val copy_args = map snd (mk_projs dbinds copy_arg)
    6.27 -    fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
    6.28 +    fun one_copy_rhs (rep_abs, (_, rhsT)) =
    6.29        let
    6.30          val body = map_of_typ thy (newTs ~~ copy_args) rhsT
    6.31        in
    6.32 @@ -257,7 +253,7 @@
    6.33        end
    6.34  
    6.35      (* define take constants *)
    6.36 -    fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy =
    6.37 +    fun define_take_const ((dbind, take_rhs), (lhsT, _)) thy =
    6.38        let
    6.39          val take_type = HOLogic.natT --> lhsT ->> lhsT
    6.40          val take_bind = Binding.suffix_name "_take" dbind
    6.41 @@ -285,7 +281,7 @@
    6.42        fold_map prove_chain_take (take_consts ~~ dbinds) thy
    6.43  
    6.44      (* prove take_0 lemmas *)
    6.45 -    fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy =
    6.46 +    fun prove_take_0 ((take_const, dbind), (lhsT, _)) thy =
    6.47        let
    6.48          val lhs = take_const $ @{term "0::nat"}
    6.49          val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT))
    6.50 @@ -302,7 +298,7 @@
    6.51      val n = Free ("n", natT)
    6.52      val take_is = map (fn t => t $ n) take_consts
    6.53      fun prove_take_Suc
    6.54 -          (((take_const, rep_abs), dbind), (lhsT, rhsT)) thy =
    6.55 +          (((take_const, rep_abs), dbind), (_, rhsT)) thy =
    6.56        let
    6.57          val lhs = take_const $ (@{term Suc} $ n)
    6.58          val body = map_of_typ thy (newTs ~~ take_is) rhsT
    6.59 @@ -326,9 +322,6 @@
    6.60          val n = Free ("n", natT)
    6.61          fun mk_goal take_const = mk_deflation (take_const $ n)
    6.62          val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts))
    6.63 -        val adm_rules =
    6.64 -          @{thms adm_conj adm_subst [OF _ adm_deflation]
    6.65 -                 cont2cont_fst cont2cont_snd cont_id}
    6.66          val bottom_rules =
    6.67            take_0_thms @ @{thms deflation_bottom simp_thms}
    6.68          val deflation_rules =
    6.69 @@ -345,7 +338,7 @@
    6.70                     ORELSE resolve_tac deflation_rules 1
    6.71                     ORELSE atac 1)])
    6.72        end
    6.73 -    fun conjuncts [] thm = []
    6.74 +    fun conjuncts [] _ = []
    6.75        | conjuncts (n::[]) thm = [(n, thm)]
    6.76        | conjuncts (n::ns) thm = let
    6.77            val thmL = thm RS @{thm conjunct1}
    6.78 @@ -378,7 +371,7 @@
    6.79        in
    6.80          add_qualified_thm "take_take" (dbind, take_take_thm) thy
    6.81        end
    6.82 -    val (take_take_thms, thy) =
    6.83 +    val (_, thy) =
    6.84        fold_map prove_take_take
    6.85          (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy
    6.86  
    6.87 @@ -391,12 +384,12 @@
    6.88        in
    6.89          add_qualified_thm "take_below" (dbind, take_below_thm) thy
    6.90        end
    6.91 -    val (take_below_thms, thy) =
    6.92 +    val (_, thy) =
    6.93        fold_map prove_take_below
    6.94          (deflation_take_thms ~~ dbinds) thy
    6.95  
    6.96      (* define finiteness predicates *)
    6.97 -    fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy =
    6.98 +    fun define_finite_const ((dbind, take_const), (lhsT, _)) thy =
    6.99        let
   6.100          val finite_type = lhsT --> boolT
   6.101          val finite_bind = Binding.suffix_name "_finite" dbind
   6.102 @@ -517,8 +510,7 @@
   6.103      val iso_infos = map snd spec
   6.104      val absTs = map #absT iso_infos
   6.105      val repTs = map #repT iso_infos
   6.106 -    val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info
   6.107 -    val {chain_take_thms, deflation_take_thms, ...} = take_info
   6.108 +    val {chain_take_thms, ...} = take_info
   6.109  
   6.110      (* prove take lemmas *)
   6.111      fun prove_take_lemma ((chain_take, lub_take), dbind) thy =
   6.112 @@ -553,12 +545,12 @@
   6.113        and finite' d (Type (c, Ts)) =
   6.114            let val d' = d andalso member (op =) types c
   6.115            in forall (finite d') Ts end
   6.116 -        | finite' d _ = true
   6.117 +        | finite' _ _ = true
   6.118      in
   6.119        val is_finite = forall (finite true) repTs
   6.120      end
   6.121  
   6.122 -    val ((finite_thms, take_induct_thms), thy) =
   6.123 +    val ((_, take_induct_thms), thy) =
   6.124        if is_finite
   6.125        then
   6.126          let
     7.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Aug 08 16:57:37 2011 -0700
     7.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Aug 08 18:36:32 2011 -0700
     7.3 @@ -102,7 +102,7 @@
     7.4      fun new_cont_tac f' i =
     7.5        case all_cont_thms f' of
     7.6          [] => no_tac
     7.7 -      | (c::cs) => rtac c i
     7.8 +      | (c::_) => rtac c i
     7.9  
    7.10      fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
    7.11        let
     8.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Aug 08 16:57:37 2011 -0700
     8.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon Aug 08 18:36:32 2011 -0700
     8.3 @@ -154,10 +154,7 @@
     8.4  
     8.5  (* prepare_cpodef *)
     8.6  
     8.7 -fun declare_type_name a =
     8.8 -  Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)))
     8.9 -
    8.10 -fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy =
    8.11 +fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy =
    8.12    let
    8.13      val _ = Theory.requires thy "Cpodef" "cpodefs"
    8.14  
    8.15 @@ -186,7 +183,7 @@
    8.16  fun add_podef def opt_name typ set opt_morphs tac thy =
    8.17    let
    8.18      val name = the_default (#1 typ) opt_name
    8.19 -    val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy) = thy
    8.20 +    val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
    8.21        |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac
    8.22      val oldT = #rep_type (#1 info)
    8.23      val newT = #abs_type (#1 info)
    8.24 @@ -216,7 +213,7 @@
    8.25        (thy: theory)
    8.26      : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
    8.27    let
    8.28 -    val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
    8.29 +    val (newT, oldT, set, morphs) =
    8.30        prepare prep_term name typ raw_set opt_morphs thy
    8.31  
    8.32      val goal_nonempty =
    8.33 @@ -249,7 +246,7 @@
    8.34        (thy: theory)
    8.35      : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
    8.36    let
    8.37 -    val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
    8.38 +    val (newT, oldT, set, morphs) =
    8.39        prepare prep_term name typ raw_set opt_morphs thy
    8.40  
    8.41      val goal_bottom_mem =
     9.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Mon Aug 08 16:57:37 2011 -0700
     9.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Mon Aug 08 18:36:32 2011 -0700
     9.3 @@ -76,14 +76,11 @@
     9.4  
     9.5  (* proving class instances *)
     9.6  
     9.7 -fun declare_type_name a =
     9.8 -  Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)))
     9.9 -
    9.10  fun gen_add_domaindef
    9.11        (prep_term: Proof.context -> 'a -> term)
    9.12        (def: bool)
    9.13        (name: binding)
    9.14 -      (typ as (tname, raw_args, mx) : binding * (string * sort) list * mixfix)
    9.15 +      (typ as (tname, raw_args, _) : binding * (string * sort) list * mixfix)
    9.16        (raw_defl: 'a)
    9.17        (opt_morphs: (binding * binding) option)
    9.18        (thy: theory)
    9.19 @@ -104,7 +101,6 @@
    9.20  
    9.21      (*lhs*)
    9.22      val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt) raw_args
    9.23 -    val lhs_sorts = map snd lhs_tfrees
    9.24      val full_tname = Sign.full_name thy tname
    9.25      val newT = Type (full_tname, map TFree lhs_tfrees)
    9.26  
    10.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Mon Aug 08 16:57:37 2011 -0700
    10.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon Aug 08 18:36:32 2011 -0700
    10.3 @@ -28,8 +28,6 @@
    10.4  val def_cont_fix_ind = @{thm def_cont_fix_ind}
    10.5  
    10.6  fun fixrec_err s = error ("fixrec definition error:\n" ^ s)
    10.7 -fun fixrec_eq_err thy s eq =
    10.8 -  fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq))
    10.9  
   10.10  (*************************************************************************)
   10.11  (***************************** building types ****************************)
   10.12 @@ -41,13 +39,10 @@
   10.13    | binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
   10.14    | binder_cfun _   =  []
   10.15  
   10.16 -fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U
   10.17 -  | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
   10.18 +fun body_cfun (Type(@{type_name cfun},[_, U])) = body_cfun U
   10.19 +  | body_cfun (Type(@{type_name "fun"},[_, U])) = body_cfun U
   10.20    | body_cfun T   =  T
   10.21  
   10.22 -fun strip_cfun T : typ list * typ =
   10.23 -  (binder_cfun T, body_cfun T)
   10.24 -
   10.25  in
   10.26  
   10.27  fun matcherT (T, U) =
   10.28 @@ -65,10 +60,9 @@
   10.29  fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)
   10.30  
   10.31  (* similar to Thm.head_of, but for continuous application *)
   10.32 -fun chead_of (Const(@{const_name Rep_cfun},_)$f$t) = chead_of f
   10.33 +fun chead_of (Const(@{const_name Rep_cfun},_)$f$_) = chead_of f
   10.34    | chead_of u = u
   10.35  
   10.36 -infix 0 ==  val (op ==) = Logic.mk_equals
   10.37  infix 1 === val (op ===) = HOLogic.mk_eq
   10.38  
   10.39  fun mk_mplus (t, u) =
   10.40 @@ -102,8 +96,8 @@
   10.41  
   10.42  local
   10.43  
   10.44 -fun name_of (Const (n, T)) = n
   10.45 -  | name_of (Free (n, T)) = n
   10.46 +fun name_of (Const (n, _)) = n
   10.47 +  | name_of (Free (n, _)) = n
   10.48    | name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t])
   10.49  
   10.50  val lhs_name =
   10.51 @@ -145,7 +139,7 @@
   10.52          Goal.prove lthy [] [] prop (K tac)
   10.53        end
   10.54  
   10.55 -    fun one_def (l as Free(n,_)) r =
   10.56 +    fun one_def (Free(n,_)) r =
   10.57            let val b = Long_Name.base_name n
   10.58            in ((Binding.name (b^"_def"), []), r) end
   10.59        | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"
   10.60 @@ -164,7 +158,7 @@
   10.61        |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict}
   10.62      val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
   10.63        |> Local_Defs.unfold lthy @{thms split_conv}
   10.64 -    fun unfolds [] thm = []
   10.65 +    fun unfolds [] _ = []
   10.66        | unfolds (n::[]) thm = [(n, thm)]
   10.67        | unfolds (n::ns) thm = let
   10.68            val thmL = thm RS @{thm Pair_eqD1}
   10.69 @@ -184,7 +178,7 @@
   10.70        in
   10.71          ((thm_name, [src]), [thm])
   10.72        end
   10.73 -    val (thmss, lthy) = lthy
   10.74 +    val (_, lthy) = lthy
   10.75        |> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms)
   10.76    in
   10.77      (lthy, names, fixdef_thms, map snd unfold_thms)
   10.78 @@ -303,7 +297,7 @@
   10.79        else HOLogic.dest_Trueprop (Logic.strip_imp_concl t)
   10.80      fun tac (t, i) =
   10.81        let
   10.82 -        val (c, T) =
   10.83 +        val (c, _) =
   10.84              (dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t
   10.85          val unfold_thm = the (Symtab.lookup tab c)
   10.86          val rule = unfold_thm RS @{thm ssubst_lhs}
   10.87 @@ -346,7 +340,7 @@
   10.88      val chead_of_spec =
   10.89        chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd
   10.90      fun name_of (Free (n, _)) = n
   10.91 -      | name_of t = fixrec_err ("unknown term")
   10.92 +      | name_of _ = fixrec_err ("unknown term")
   10.93      val all_names = map (name_of o chead_of_spec) spec
   10.94      val names = distinct (op =) all_names
   10.95      fun block_of_name n =
   10.96 @@ -362,7 +356,7 @@
   10.97  
   10.98      val matches = map (compile_eqs match_name) (map (map (snd o fst)) blocks)
   10.99      val spec' = map (pair Attrib.empty_binding) matches
  10.100 -    val (lthy, cnames, fixdef_thms, unfold_thms) =
  10.101 +    val (lthy, _, _, unfold_thms) =
  10.102        add_fixdefs fixes spec' lthy
  10.103  
  10.104      val blocks' = map (map fst o filter_out snd) blocks
    11.1 --- a/src/HOL/HOLCF/Tools/holcf_library.ML	Mon Aug 08 16:57:37 2011 -0700
    11.2 +++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Mon Aug 08 18:36:32 2011 -0700
    11.3 @@ -244,7 +244,7 @@
    11.4      (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V)
    11.5  
    11.6  fun mk_sscase (t, u) =
    11.7 -  let val (T, V) = dest_cfunT (fastype_of t)
    11.8 +  let val (T, _) = dest_cfunT (fastype_of t)
    11.9        val (U, V) = dest_cfunT (fastype_of u)
   11.10    in sscase_const (T, U, V) ` t ` u end
   11.11