src/HOL/HOLCF/Tools/Domain/domain.ML

 
 open HOLCF_Library
 
 fun first  (x,_,_) = x
 fun second (_,x,_) = x
-fun third  (_,_,x) = x
 
 (* ----- calls for building new thy and thms -------------------------------- *)
 
 type info =
      Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info

         map (fn (_,dbind,_,_) => dbind) raw_specs
     val raw_rhss :
         (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)
 
     fun test_dupl_tvars s =
       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'
       in
         case distinct (eq_set (op =)) all_sorts of

 
     (* test for free type variables, illegal sort constraints on rhs,
        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)) =
         (case AList.lookup (op =) dtnvs' s of
           NONE =>

                   NONE => T
                 | SOME c =>
                   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
         val T = prep_typ tmp_thy sorts raw_T
         val _ = check_rec NONE T

     fun prep_con (b, args, mx) = (b, map prep_arg args, mx)
     fun prep_rhs cons = map prep_con cons
     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)
 
     val absTs : typ list = map Type dtnvs'
     val repTs : typ list = map mk_rhs_typ rhss

         thy
           |> fold_map (fn ((dbind, cons), info) =>
                 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
     thy
   end
 
 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)
   end