# HG changeset patch
# User huffman
# Date 1312853792 25200
# Node ID 53d95b52954c5725827f9bdbf56cbb09c99d5cf0
# Parent  bcc60791b7b92db201217f029265cd4f0474b5be
HOLCF: fix warnings about unreferenced identifiers

diff -r bcc60791b7b9 -r 53d95b52954c src/HOL/HOLCF/Tools/Domain/domain.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon Aug 08 18:36:32 2011 -0700
@@ -35,7 +35,6 @@
 
 fun first  (x,_,_) = x
 fun second (_,x,_) = x
-fun third  (_,_,x) = x
 
 (* ----- calls for building new thy and thms -------------------------------- *)
 
@@ -78,16 +77,16 @@
         (binding * (bool * binding option * 'b) list * mixfix) list list =
         map (fn (_,_,_,cons) => cons) raw_specs
     val dtnvs' : (string * typ list) list =
-        map (fn (dbind, vs, mx) => (Sign.full_name thy dbind, vs)) dtnvs
+        map (fn (dbind, vs, _) => (Sign.full_name thy dbind, vs)) dtnvs
 
     val all_cons = map (Binding.name_of o first) (flat raw_rhss)
-    val test_dupl_cons =
+    val _ =
       case duplicates (op =) all_cons of 
         [] => false | dups => error ("Duplicate constructors: " 
                                       ^ commas_quote dups)
     val all_sels =
       (map Binding.name_of o map_filter second o maps second) (flat raw_rhss)
-    val test_dupl_sels =
+    val _ =
       case duplicates (op =) all_sels of
         [] => false | dups => error("Duplicate selectors: "^commas_quote dups)
 
@@ -95,7 +94,7 @@
       case duplicates (op =) (map(fst o dest_TFree)s) of
         [] => false | dups => error("Duplicate type arguments: " 
                                     ^commas_quote dups)
-    val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs')
+    val _ = exists test_dupl_tvars (map snd dtnvs')
 
     val sorts : (string * sort) list =
       let val all_sorts = map (map dest_TFree o snd) dtnvs'
@@ -119,7 +118,7 @@
        non-pcpo-types and invalid use of recursive type
        replace sorts in type variables on rhs *)
     val rec_tab = Domain_Take_Proofs.get_rec_tab thy
-    fun check_rec no_rec (T as TFree (v,_))  =
+    fun check_rec _ (T as TFree (v,_))  =
         if AList.defined (op =) sorts v then T
         else error ("Free type variable " ^ quote v ^ " on rhs.")
       | check_rec no_rec (T as Type (s, Ts)) =
@@ -141,7 +140,7 @@
                   error ("Illegal indirect recursion of type " ^ 
                          quote (Syntax.string_of_typ_global tmp_thy T) ^
                          " under type constructor " ^ quote c)))
-      | check_rec no_rec (TVar _) = error "extender:check_rec"
+      | check_rec _ (TVar _) = error "extender:check_rec"
 
     fun prep_arg (lazy, sel, raw_T) =
       let
@@ -154,8 +153,8 @@
     val rhss : (binding * (bool * binding option * typ) list * mixfix) list list =
         map prep_rhs raw_rhss
 
-    fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T
-    fun mk_con_typ (bind, args, mx) =
+    fun mk_arg_typ (lazy, _, T) = if lazy then mk_upT T else T
+    fun mk_con_typ (_, args, _) =
         if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args)
     fun mk_rhs_typ cons = foldr1 mk_ssumT (map mk_con_typ cons)
 
@@ -174,7 +173,7 @@
                 Domain_Constructors.add_domain_constructors dbind cons info)
              (dbinds ~~ rhss ~~ iso_infos)
 
-    val (take_rews, thy) =
+    val (_, thy) =
         Domain_Induction.comp_theorems
           dbinds take_info constr_infos thy
   in
@@ -184,7 +183,7 @@
 fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
   let
     fun prep (dbind, mx, (lhsT, rhsT)) =
-      let val (dname, vs) = dest_Type lhsT
+      let val (_, vs) = dest_Type lhsT
       in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end
   in
     Domain_Isomorphism.domain_isomorphism (map prep spec)
diff -r bcc60791b7b9 -r 53d95b52954c src/HOL/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Mon Aug 08 18:36:32 2011 -0700
@@ -127,7 +127,7 @@
           (dbinds ~~ iso_infos) take_info lub_take_thms thy
 
     (* define map functions *)
-    val (map_info, thy) =
+    val (_, thy) =
         Domain_Isomorphism.define_map_functions
           (dbinds ~~ iso_infos) thy
 
diff -r bcc60791b7b9 -r 53d95b52954c src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Mon Aug 08 18:36:32 2011 -0700
@@ -80,9 +80,9 @@
     fun mk_decl (b, t, mx) = (b, fastype_of t, mx)
     val decls = map mk_decl specs
     val thy = Cont_Consts.add_consts decls thy
-    fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T)
+    fun mk_const (b, T, _) = Const (Sign.full_name thy b, T)
     val consts = map mk_const decls
-    fun mk_def c (b, t, mx) =
+    fun mk_def c (b, t, _) =
       (Binding.suffix_name "_def" b, Logic.mk_equals (c, t))
     val defs = map2 mk_def consts specs
     val (def_thms, thy) =
@@ -159,7 +159,7 @@
     val abs_strict = iso_locale RS @{thm iso.abs_strict}
 
     (* get types of type isomorphism *)
-    val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const)
+    val (_, lhsT) = dest_cfunT (fastype_of abs_const)
 
     fun vars_of args =
       let
@@ -172,7 +172,7 @@
     (* define constructor functions *)
     val ((con_consts, con_defs), thy) =
       let
-        fun one_arg (lazy, T) var = if lazy then mk_up var else var
+        fun one_arg (lazy, _) var = if lazy then mk_up var else var
         fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args))
         fun mk_abs t = abs_const ` t
         val rhss = map mk_abs (mk_sinjects (map one_con spec))
@@ -187,13 +187,13 @@
 
     (* replace bindings with terms in constructor spec *)
     val spec' : (term * (bool * typ) list) list =
-      let fun one_con con (b, args, mx) = (con, args)
+      let fun one_con con (_, args, _) = (con, args)
       in map2 one_con con_consts spec end
 
     (* prove exhaustiveness of constructors *)
     local
-      fun arg2typ n (true,  T) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo})))
-        | arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo}))
+      fun arg2typ n (true,  _) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo})))
+        | arg2typ n (false, _) = (n+1, TVar (("'a", n), @{sort pcpo}))
       fun args2typ n [] = (n, oneT)
         | args2typ n [arg] = arg2typ n arg
         | args2typ n (arg::args) =
@@ -332,14 +332,14 @@
         | prime t             = t
       fun iff_disj (t, []) = mk_not t
         | iff_disj (t, ts) = mk_eq (t, foldr1 mk_disj ts)
-      fun iff_disj2 (t, [], us) = mk_not t
-        | iff_disj2 (t, ts, []) = mk_not t
+      fun iff_disj2 (t, [], _) = mk_not t
+        | iff_disj2 (t, _, []) = mk_not t
         | iff_disj2 (t, ts, us) =
           mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us))
       fun dist_le (con1, args1) (con2, args2) =
         let
           val (vs1, zs1) = get_vars args1
-          val (vs2, zs2) = get_vars args2 |> pairself (map prime)
+          val (vs2, _) = get_vars args2 |> pairself (map prime)
           val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2))
           val rhss = map mk_undef zs1
           val goal = mk_trp (iff_disj (lhs, rhss))
@@ -390,7 +390,6 @@
     (lhsT : typ)
     (dbind : binding)
     (con_betas : thm list)
-    (exhaust : thm)
     (iso_locale : thm)
     (rep_const : term)
     (thy : theory)
@@ -429,7 +428,7 @@
         | mk_sscases ts = foldr1 mk_sscase ts
       val body = mk_sscases (map2 one_con fs spec)
       val rhs = big_lambdas fs (mk_cfcomp (body, rep_const))
-      val ((case_consts, case_defs), thy) =
+      val ((_, case_defs), thy) =
           define_consts [(case_bind, rhs, NoSyn)] thy
       val case_name = Sign.full_name thy case_bind
     in
@@ -457,7 +456,7 @@
           Library.foldl capp (c_ast authentic con, argvars n args)
       fun case1 authentic (n, c) =
           app "_case1" (Ast.strip_positions (con1 authentic n c), expvar n)
-      fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
+      fun arg1 (n, (_, args)) = List.foldr cabs (expvar n) (argvars n args)
       fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
       val case_constant = Ast.Constant (syntax (case_const dummyT))
       fun case_trans authentic =
@@ -541,16 +540,16 @@
         fun mk_ssnd s = mk_cfcomp (ssnd_const (dest_sprodT (rangeT s)), s)
         fun mk_down s = mk_cfcomp (from_up (dest_upT (rangeT s)), s)
 
-        fun sels_of_arg s (lazy, NONE,   T) = []
-          | sels_of_arg s (lazy, SOME b, T) =
+        fun sels_of_arg _ (_, NONE, _) = []
+          | sels_of_arg s (lazy, SOME b, _) =
             [(b, if lazy then mk_down s else s, NoSyn)]
-        fun sels_of_args s [] = []
+        fun sels_of_args _ [] = []
           | sels_of_args s (v :: []) = sels_of_arg s v
           | sels_of_args s (v :: vs) =
             sels_of_arg (mk_sfst s) v @ sels_of_args (mk_ssnd s) vs
-        fun sels_of_cons s [] = []
-          | sels_of_cons s ((con, args) :: []) = sels_of_args s args
-          | sels_of_cons s ((con, args) :: cs) =
+        fun sels_of_cons _ [] = []
+          | sels_of_cons s ((_, args) :: []) = sels_of_args s args
+          | sels_of_cons s ((_, args) :: cs) =
             sels_of_args (mk_outl s) args @ sels_of_cons (mk_outr s) cs
         val sel_eqns : (binding * term * mixfix) list =
             sels_of_cons rep_const spec
@@ -598,7 +597,7 @@
             val vs : term list = map Free (ns ~~ Ts)
             val con_app : term = list_ccomb (con, vs)
             val vs' : (bool * term) list = map #1 args ~~ vs
-            fun one_same (n, sel, T) =
+            fun one_same (n, sel, _) =
               let
                 val xs = map snd (filter_out fst (nth_drop n vs'))
                 val assms = map (mk_trp o mk_defined) xs
@@ -607,7 +606,7 @@
               in
                 prove thy defs goal (K tacs)
               end
-            fun one_diff (n, sel, T) =
+            fun one_diff (_, sel, T) =
               let
                 val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T))
               in
@@ -615,8 +614,8 @@
               end
             fun one_con (j, (_, args')) : thm list =
               let
-                fun prep (i, (lazy, NONE, T)) = NONE
-                  | prep (i, (lazy, SOME sel, T)) = SOME (i, sel, T)
+                fun prep (_, (_, NONE, _)) = NONE
+                  | prep (i, (_, SOME sel, T)) = SOME (i, sel, T)
                 val sels : (int * term * typ) list =
                   map_filter prep (map_index I args')
               in
@@ -646,12 +645,12 @@
           in
             prove thy sel_defs goal (K tacs)
           end
-        fun one_arg (false, SOME sel, T) = SOME (sel_defin sel)
+        fun one_arg (false, SOME sel, _) = SOME (sel_defin sel)
           | one_arg _                    = NONE
       in
         case spec2 of
-          [(con, args)] => map_filter one_arg args
-        | _             => []
+          [(_, args)] => map_filter one_arg args
+        | _           => []
       end
 
   in
@@ -672,19 +671,11 @@
     (thy : theory) =
   let
 
-    fun vars_of args =
-      let
-        val Ts = map snd args
-        val ns = Datatype_Prop.make_tnames Ts
-      in
-        map Free (ns ~~ Ts)
-      end
-
     (* define discriminator functions *)
     local
-      fun dis_fun i (j, (con, args)) =
+      fun dis_fun i (j, (_, args)) =
         let
-          val (vs, nonlazy) = get_vars args
+          val (vs, _) = get_vars args
           val tr = if i = j then @{term TT} else @{term FF}
         in
           big_lambdas vs tr
@@ -758,7 +749,6 @@
     (bindings : binding list)
     (spec : (term * (bool * typ) list) list)
     (lhsT : typ)
-    (exhaust : thm)
     (case_const : typ -> term)
     (case_rews : thm list)
     (thy : theory) =
@@ -776,13 +766,13 @@
       val x = Free ("x", lhsT)
       fun k args = Free ("k", map snd args -->> mk_matchT resultT)
       val fail = mk_fail resultT
-      fun mat_fun i (j, (con, args)) =
+      fun mat_fun i (j, (_, args)) =
         let
-          val (vs, nonlazy) = get_vars_avoiding ["x","k"] args
+          val (vs, _) = get_vars_avoiding ["x","k"] args
         in
           if i = j then k args else big_lambdas vs fail
         end
-      fun mat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
+      fun mat_eqn (i, (bind, (_, args))) : binding * term * mixfix =
         let
           val mat_bind = Binding.prefix_name "match_" bind
           val funs = map_index (mat_fun i) spec
@@ -866,7 +856,6 @@
     val rep_strict = iso_locale RS @{thm iso.rep_strict}
     val abs_strict = iso_locale RS @{thm iso.abs_strict}
     val rep_bottom_iff = iso_locale RS @{thm iso.rep_bottom_iff}
-    val abs_bottom_iff = iso_locale RS @{thm iso.abs_bottom_iff}
     val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict]
 
     (* qualify constants and theorems with domain name *)
@@ -875,7 +864,7 @@
     (* define constructor functions *)
     val (con_result, thy) =
       let
-        fun prep_arg (lazy, sel, T) = (lazy, T)
+        fun prep_arg (lazy, _, T) = (lazy, T)
         fun prep_con (b, args, mx) = (b, map prep_arg args, mx)
         val con_spec = map prep_con spec
       in
@@ -887,8 +876,8 @@
     (* prepare constructor spec *)
     val con_specs : (term * (bool * typ) list) list =
       let
-        fun prep_arg (lazy, sel, T) = (lazy, T)
-        fun prep_con c (b, args, mx) = (c, map prep_arg args)
+        fun prep_arg (lazy, _, T) = (lazy, T)
+        fun prep_con c (_, args, _) = (c, map prep_arg args)
       in
         map2 prep_con con_consts spec
       end
@@ -896,13 +885,13 @@
     (* define case combinator *)
     val ((case_const : typ -> term, cases : thm list), thy) =
         add_case_combinator con_specs lhsT dbind
-          con_betas exhaust iso_locale rep_const thy
+          con_betas iso_locale rep_const thy
 
     (* define and prove theorems for selector functions *)
     val (sel_thms : thm list, thy : theory) =
       let
         val sel_spec : (term * (bool * binding option * typ) list) list =
-          map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec
+          map2 (fn con => fn (_, args, _) => (con, args)) con_consts spec
       in
         add_selectors sel_spec rep_const
           abs_iso_thm rep_strict rep_bottom_iff con_betas thy
@@ -916,7 +905,7 @@
     (* define and prove theorems for match combinators *)
     val (match_thms : thm list, thy : theory) =
         add_match_combinators bindings con_specs lhsT
-          exhaust case_const cases thy
+          case_const cases thy
 
     (* restore original signature path *)
     val thy = Sign.parent_path thy
diff -r bcc60791b7b9 -r 53d95b52954c src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Mon Aug 08 18:36:32 2011 -0700
@@ -221,7 +221,7 @@
           if length dnames = 1 then ["bottom"] else
           map (fn s => "bottom_" ^ Long_Name.base_name s) dnames
       fun one_eq bot (constr_info : Domain_Constructors.constr_info) =
-        let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c))
+        let fun name_of (c, _) = Long_Name.base_name (fst (dest_Const c))
         in bot :: map name_of (#con_specs constr_info) end
     in adms @ flat (map2 one_eq bottoms constr_infos) end
 
@@ -344,7 +344,7 @@
       val assm1 = mk_trp (list_comb (bisim_const, Rs))
       val assm2 = mk_trp (R $ x $ y)
       val goal = mk_trp (mk_eq (x, y))
-      fun tacf {prems, context} =
+      fun tacf {prems, context = _} =
         let
           val rule = hd prems RS coind_lemma
         in
@@ -420,7 +420,7 @@
 val (take_rewss, thy) =
     take_theorems dbinds take_info constr_infos thy
 
-val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info
+val {take_0_thms, take_strict_thms, ...} = take_info
 
 val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss
 
diff -r bcc60791b7b9 -r 53d95b52954c src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Aug 08 18:36:32 2011 -0700
@@ -86,15 +86,6 @@
 
 fun mk_u_defl t = mk_capply (@{const "u_defl"}, t)
 
-fun mk_u_map t =
-  let
-    val (T, U) = dest_cfunT (fastype_of t)
-    val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U)
-    val u_map_const = Const (@{const_name u_map}, u_map_type)
-  in
-    mk_capply (u_map_const, t)
-  end
-
 fun emb_const T = Const (@{const_name emb}, T ->> udomT)
 fun prj_const T = Const (@{const_name prj}, udomT ->> T)
 fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T)
@@ -130,7 +121,7 @@
 (*************** fixed-point definitions and unfolding theorems ***************)
 (******************************************************************************)
 
-fun mk_projs []      t = []
+fun mk_projs []      _ = []
   | mk_projs (x::[]) t = [(x, t)]
   | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t)
 
@@ -187,7 +178,7 @@
       (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
       |> Local_Defs.unfold (Proof_Context.init_global thy) @{thms split_conv}
 
-    fun mk_unfold_thms [] thm = []
+    fun mk_unfold_thms [] _ = []
       | mk_unfold_thms (n::[]) thm = [(n, thm)]
       | mk_unfold_thms (n::ns) thm = let
           val thmL = thm RS @{thm Pair_eqD1}
@@ -271,7 +262,7 @@
       | mapT T = T ->> T
 
     (* declare map functions *)
-    fun declare_map_const (tbind, (lhsT, rhsT)) thy =
+    fun declare_map_const (tbind, (lhsT, _)) thy =
       let
         val map_type = mapT lhsT
         val map_bind = Binding.suffix_name "_map" tbind
@@ -290,7 +281,7 @@
       val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns)
       val Ts = (snd o dest_Type o fst o hd) dom_eqns
       val tab = (Ts ~~ map mapvar Ts) @ tab1
-      fun mk_map_spec (((rep_const, abs_const), map_const), (lhsT, rhsT)) =
+      fun mk_map_spec (((rep_const, abs_const), _), (lhsT, rhsT)) =
         let
           val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT
           val body = Domain_Take_Proofs.map_of_typ thy tab rhsT
@@ -313,7 +304,7 @@
         fun unprime a = Library.unprefix "'" a
         fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T)
         fun mk_assm T = mk_trp (mk_deflation (mk_f T))
-        fun mk_goal (map_const, (lhsT, rhsT)) =
+        fun mk_goal (map_const, (lhsT, _)) =
           let
             val (_, Ts) = dest_Type lhsT
             val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
@@ -343,7 +334,7 @@
            REPEAT (etac @{thm conjE} 1),
            REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)])
       end
-    fun conjuncts [] thm = []
+    fun conjuncts [] _ = []
       | conjuncts (n::[]) thm = [(n, thm)]
       | conjuncts (n::ns) thm = let
           val thmL = thm RS @{thm conjunct1}
@@ -360,7 +351,6 @@
       fun register_map (dname, args) =
         Domain_Take_Proofs.add_rec_type (dname, args)
       val dnames = map (fst o dest_Type o fst) dom_eqns
-      val map_names = map (fst o dest_Const) map_consts
       fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => []
       val argss = map args dom_eqns
     in
@@ -417,7 +407,7 @@
     (* this theory is used just for parsing *)
     val tmp_thy = thy |>
       Theory.copy |>
-      Sign.add_types_global (map (fn (tvs, tbind, mx, _, morphs) =>
+      Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) =>
         (tbind, length tvs, mx)) doms_raw)
 
     fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts =
@@ -434,28 +424,28 @@
     (* declare arities in temporary theory *)
     val tmp_thy =
       let
-        fun arity (vs, tbind, mx, _, _) =
+        fun arity (vs, tbind, _, _, _) =
           (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"})
       in
         fold AxClass.axiomatize_arity (map arity doms) tmp_thy
       end
 
     (* check bifiniteness of right-hand sides *)
-    fun check_rhs (vs, tbind, mx, rhs, morphs) =
+    fun check_rhs (_, _, _, rhs, _) =
       if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then ()
       else error ("Type not of sort domain: " ^
         quote (Syntax.string_of_typ_global tmp_thy rhs))
     val _ = map check_rhs doms
 
     (* domain equations *)
-    fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) =
+    fun mk_dom_eqn (vs, tbind, _, rhs, _) =
       let fun arg v = TFree (v, the_sort v)
       in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end
     val dom_eqns = map mk_dom_eqn doms
 
     (* check for valid type parameters *)
     val (tyvars, _, _, _, _) = hd doms
-    val new_doms = map (fn (tvs, tname, mx, _, _) =>
+    val _ = map (fn (tvs, tname, _, _, _) =>
       let val full_tname = Sign.full_name tmp_thy tname
       in
         (case duplicates (op =) tvs of
@@ -528,7 +518,7 @@
     fun make_repdef ((vs, tbind, mx, _, _), defl) thy =
       let
         val spec = (tbind, map (rpair dummyS) vs, mx)
-        val ((_, _, _, {DEFL, liftemb_def, liftprj_def, ...}), thy) =
+        val ((_, _, _, {DEFL, ...}), thy) =
           Domaindef.add_domaindef false NONE spec defl NONE thy
         (* declare domain_defl_simps rules *)
         val thy = Context.theory_map (RepData.add_thm DEFL) thy
@@ -557,7 +547,7 @@
         (DEFL_eq_binds ~~ DEFL_eq_thms)
 
     (* define rep/abs functions *)
-    fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy =
+    fun mk_rep_abs ((tbind, _), (lhsT, rhsT)) thy =
       let
         val rep_bind = Binding.suffix_name "_rep" tbind
         val abs_bind = Binding.suffix_name "_abs" tbind
@@ -611,8 +601,7 @@
     (* definitions and proofs related to map functions *)
     val (map_info, thy) =
         define_map_functions (dbinds ~~ iso_infos) thy
-    val { map_consts, map_apply_thms, map_unfold_thms,
-          map_cont_thm, deflation_map_thms } = map_info
+    val { map_consts, map_apply_thms, map_cont_thm, ...} = map_info
 
     (* prove isodefl rules for map functions *)
     val isodefl_thm =
@@ -627,7 +616,7 @@
           | NONE =>
             let val T = dest_DEFL t
             in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end
-        fun mk_goal (map_const, (T, rhsT)) =
+        fun mk_goal (map_const, (T, _)) =
           let
             val (_, Ts) = dest_Type T
             val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
@@ -662,7 +651,7 @@
            REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
       end
     val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds
-    fun conjuncts [] thm = []
+    fun conjuncts [] _ = []
       | conjuncts (n::[]) thm = [(n, thm)]
       | conjuncts (n::ns) thm = let
           val thmL = thm RS @{thm conjunct1}
@@ -709,7 +698,7 @@
       let
         val lhs = mk_tuple (map mk_lub take_consts)
         fun is_cpo T = Sign.of_sort thy (T, @{sort cpo})
-        fun mk_map_ID (map_const, (lhsT, rhsT)) =
+        fun mk_map_ID (map_const, (lhsT, _)) =
           list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT))))
         val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns))
         val goal = mk_trp (mk_eq (lhs, rhs))
@@ -736,7 +725,7 @@
       end
 
     (* prove lub of take equals ID *)
-    fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
+    fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, _)) thy =
       let
         val n = Free ("n", natT)
         val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT)
diff -r bcc60791b7b9 -r 53d95b52954c src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Aug 08 18:36:32 2011 -0700
@@ -159,10 +159,6 @@
 infix -->>
 infix 9 `
 
-fun mapT (T as Type (_, Ts)) =
-    (map (fn T => T ->> T) Ts) -->> (T ->> T)
-  | mapT T = T ->> T
-
 fun mk_deflation t =
   Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t
 
@@ -227,7 +223,7 @@
     val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos
     val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos
 
-    fun mk_projs []      t = []
+    fun mk_projs []      _ = []
       | mk_projs (x::[]) t = [(x, t)]
       | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t)
 
@@ -239,7 +235,7 @@
     val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs)
     val copy_arg = Free ("f", copy_arg_type)
     val copy_args = map snd (mk_projs dbinds copy_arg)
-    fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
+    fun one_copy_rhs (rep_abs, (_, rhsT)) =
       let
         val body = map_of_typ thy (newTs ~~ copy_args) rhsT
       in
@@ -257,7 +253,7 @@
       end
 
     (* define take constants *)
-    fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy =
+    fun define_take_const ((dbind, take_rhs), (lhsT, _)) thy =
       let
         val take_type = HOLogic.natT --> lhsT ->> lhsT
         val take_bind = Binding.suffix_name "_take" dbind
@@ -285,7 +281,7 @@
       fold_map prove_chain_take (take_consts ~~ dbinds) thy
 
     (* prove take_0 lemmas *)
-    fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy =
+    fun prove_take_0 ((take_const, dbind), (lhsT, _)) thy =
       let
         val lhs = take_const $ @{term "0::nat"}
         val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT))
@@ -302,7 +298,7 @@
     val n = Free ("n", natT)
     val take_is = map (fn t => t $ n) take_consts
     fun prove_take_Suc
-          (((take_const, rep_abs), dbind), (lhsT, rhsT)) thy =
+          (((take_const, rep_abs), dbind), (_, rhsT)) thy =
       let
         val lhs = take_const $ (@{term Suc} $ n)
         val body = map_of_typ thy (newTs ~~ take_is) rhsT
@@ -326,9 +322,6 @@
         val n = Free ("n", natT)
         fun mk_goal take_const = mk_deflation (take_const $ n)
         val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts))
-        val adm_rules =
-          @{thms adm_conj adm_subst [OF _ adm_deflation]
-                 cont2cont_fst cont2cont_snd cont_id}
         val bottom_rules =
           take_0_thms @ @{thms deflation_bottom simp_thms}
         val deflation_rules =
@@ -345,7 +338,7 @@
                    ORELSE resolve_tac deflation_rules 1
                    ORELSE atac 1)])
       end
-    fun conjuncts [] thm = []
+    fun conjuncts [] _ = []
       | conjuncts (n::[]) thm = [(n, thm)]
       | conjuncts (n::ns) thm = let
           val thmL = thm RS @{thm conjunct1}
@@ -378,7 +371,7 @@
       in
         add_qualified_thm "take_take" (dbind, take_take_thm) thy
       end
-    val (take_take_thms, thy) =
+    val (_, thy) =
       fold_map prove_take_take
         (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy
 
@@ -391,12 +384,12 @@
       in
         add_qualified_thm "take_below" (dbind, take_below_thm) thy
       end
-    val (take_below_thms, thy) =
+    val (_, thy) =
       fold_map prove_take_below
         (deflation_take_thms ~~ dbinds) thy
 
     (* define finiteness predicates *)
-    fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy =
+    fun define_finite_const ((dbind, take_const), (lhsT, _)) thy =
       let
         val finite_type = lhsT --> boolT
         val finite_bind = Binding.suffix_name "_finite" dbind
@@ -517,8 +510,7 @@
     val iso_infos = map snd spec
     val absTs = map #absT iso_infos
     val repTs = map #repT iso_infos
-    val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info
-    val {chain_take_thms, deflation_take_thms, ...} = take_info
+    val {chain_take_thms, ...} = take_info
 
     (* prove take lemmas *)
     fun prove_take_lemma ((chain_take, lub_take), dbind) thy =
@@ -553,12 +545,12 @@
       and finite' d (Type (c, Ts)) =
           let val d' = d andalso member (op =) types c
           in forall (finite d') Ts end
-        | finite' d _ = true
+        | finite' _ _ = true
     in
       val is_finite = forall (finite true) repTs
     end
 
-    val ((finite_thms, take_induct_thms), thy) =
+    val ((_, take_induct_thms), thy) =
       if is_finite
       then
         let
diff -r bcc60791b7b9 -r 53d95b52954c src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Aug 08 18:36:32 2011 -0700
@@ -102,7 +102,7 @@
     fun new_cont_tac f' i =
       case all_cont_thms f' of
         [] => no_tac
-      | (c::cs) => rtac c i
+      | (c::_) => rtac c i
 
     fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
       let
diff -r bcc60791b7b9 -r 53d95b52954c src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon Aug 08 18:36:32 2011 -0700
@@ -154,10 +154,7 @@
 
 (* prepare_cpodef *)
 
-fun declare_type_name a =
-  Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)))
-
-fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy =
+fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy =
   let
     val _ = Theory.requires thy "Cpodef" "cpodefs"
 
@@ -186,7 +183,7 @@
 fun add_podef def opt_name typ set opt_morphs tac thy =
   let
     val name = the_default (#1 typ) opt_name
-    val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy) = thy
+    val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
       |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac
     val oldT = #rep_type (#1 info)
     val newT = #abs_type (#1 info)
@@ -216,7 +213,7 @@
       (thy: theory)
     : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
   let
-    val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
+    val (newT, oldT, set, morphs) =
       prepare prep_term name typ raw_set opt_morphs thy
 
     val goal_nonempty =
@@ -249,7 +246,7 @@
       (thy: theory)
     : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
   let
-    val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
+    val (newT, oldT, set, morphs) =
       prepare prep_term name typ raw_set opt_morphs thy
 
     val goal_bottom_mem =
diff -r bcc60791b7b9 -r 53d95b52954c src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Mon Aug 08 18:36:32 2011 -0700
@@ -76,14 +76,11 @@
 
 (* proving class instances *)
 
-fun declare_type_name a =
-  Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)))
-
 fun gen_add_domaindef
       (prep_term: Proof.context -> 'a -> term)
       (def: bool)
       (name: binding)
-      (typ as (tname, raw_args, mx) : binding * (string * sort) list * mixfix)
+      (typ as (tname, raw_args, _) : binding * (string * sort) list * mixfix)
       (raw_defl: 'a)
       (opt_morphs: (binding * binding) option)
       (thy: theory)
@@ -104,7 +101,6 @@
 
     (*lhs*)
     val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt) raw_args
-    val lhs_sorts = map snd lhs_tfrees
     val full_tname = Sign.full_name thy tname
     val newT = Type (full_tname, map TFree lhs_tfrees)
 
diff -r bcc60791b7b9 -r 53d95b52954c src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon Aug 08 18:36:32 2011 -0700
@@ -28,8 +28,6 @@
 val def_cont_fix_ind = @{thm def_cont_fix_ind}
 
 fun fixrec_err s = error ("fixrec definition error:\n" ^ s)
-fun fixrec_eq_err thy s eq =
-  fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq))
 
 (*************************************************************************)
 (***************************** building types ****************************)
@@ -41,13 +39,10 @@
   | binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
   | binder_cfun _   =  []
 
-fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U
-  | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
+fun body_cfun (Type(@{type_name cfun},[_, U])) = body_cfun U
+  | body_cfun (Type(@{type_name "fun"},[_, U])) = body_cfun U
   | body_cfun T   =  T
 
-fun strip_cfun T : typ list * typ =
-  (binder_cfun T, body_cfun T)
-
 in
 
 fun matcherT (T, U) =
@@ -65,10 +60,9 @@
 fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)
 
 (* similar to Thm.head_of, but for continuous application *)
-fun chead_of (Const(@{const_name Rep_cfun},_)$f$t) = chead_of f
+fun chead_of (Const(@{const_name Rep_cfun},_)$f$_) = chead_of f
   | chead_of u = u
 
-infix 0 ==  val (op ==) = Logic.mk_equals
 infix 1 === val (op ===) = HOLogic.mk_eq
 
 fun mk_mplus (t, u) =
@@ -102,8 +96,8 @@
 
 local
 
-fun name_of (Const (n, T)) = n
-  | name_of (Free (n, T)) = n
+fun name_of (Const (n, _)) = n
+  | name_of (Free (n, _)) = n
   | name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t])
 
 val lhs_name =
@@ -145,7 +139,7 @@
         Goal.prove lthy [] [] prop (K tac)
       end
 
-    fun one_def (l as Free(n,_)) r =
+    fun one_def (Free(n,_)) r =
           let val b = Long_Name.base_name n
           in ((Binding.name (b^"_def"), []), r) end
       | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"
@@ -164,7 +158,7 @@
       |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict}
     val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
       |> Local_Defs.unfold lthy @{thms split_conv}
-    fun unfolds [] thm = []
+    fun unfolds [] _ = []
       | unfolds (n::[]) thm = [(n, thm)]
       | unfolds (n::ns) thm = let
           val thmL = thm RS @{thm Pair_eqD1}
@@ -184,7 +178,7 @@
       in
         ((thm_name, [src]), [thm])
       end
-    val (thmss, lthy) = lthy
+    val (_, lthy) = lthy
       |> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms)
   in
     (lthy, names, fixdef_thms, map snd unfold_thms)
@@ -303,7 +297,7 @@
       else HOLogic.dest_Trueprop (Logic.strip_imp_concl t)
     fun tac (t, i) =
       let
-        val (c, T) =
+        val (c, _) =
             (dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t
         val unfold_thm = the (Symtab.lookup tab c)
         val rule = unfold_thm RS @{thm ssubst_lhs}
@@ -346,7 +340,7 @@
     val chead_of_spec =
       chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd
     fun name_of (Free (n, _)) = n
-      | name_of t = fixrec_err ("unknown term")
+      | name_of _ = fixrec_err ("unknown term")
     val all_names = map (name_of o chead_of_spec) spec
     val names = distinct (op =) all_names
     fun block_of_name n =
@@ -362,7 +356,7 @@
 
     val matches = map (compile_eqs match_name) (map (map (snd o fst)) blocks)
     val spec' = map (pair Attrib.empty_binding) matches
-    val (lthy, cnames, fixdef_thms, unfold_thms) =
+    val (lthy, _, _, unfold_thms) =
       add_fixdefs fixes spec' lthy
 
     val blocks' = map (map fst o filter_out snd) blocks
diff -r bcc60791b7b9 -r 53d95b52954c src/HOL/HOLCF/Tools/holcf_library.ML
--- a/src/HOL/HOLCF/Tools/holcf_library.ML	Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Mon Aug 08 18:36:32 2011 -0700
@@ -244,7 +244,7 @@
     (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V)
 
 fun mk_sscase (t, u) =
-  let val (T, V) = dest_cfunT (fastype_of t)
+  let val (T, _) = dest_cfunT (fastype_of t)
       val (U, V) = dest_cfunT (fastype_of u)
   in sscase_const (T, U, V) ` t ` u end