src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35521 47eec4da124a
parent 35514 a2cfa413eaab
child 35523 cc57f4a274a3
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 15:46:23 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 15:53:07 2010 -0800
     1.3 @@ -179,7 +179,7 @@
     1.4    fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict");
     1.5    val axs_take_strict = map get_take_strict dnames;
     1.6  
     1.7 -  fun one_take_app (con, _, args) =
     1.8 +  fun one_take_app (con, args) =
     1.9      let
    1.10        fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
    1.11        fun one_rhs arg =
    1.12 @@ -263,7 +263,7 @@
    1.13    val dnames = map (fst o fst) eqs;
    1.14    val x_name = idx_name dnames "x"; 
    1.15  
    1.16 -  fun one_con (con, _, args) =
    1.17 +  fun one_con (con, args) =
    1.18      let
    1.19        val nonrec_args = filter_out is_rec args;
    1.20        val    rec_args = filter is_rec args;
    1.21 @@ -343,7 +343,7 @@
    1.22      maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
    1.23  
    1.24  local
    1.25 -  fun one_con p (con, _, args) =
    1.26 +  fun one_con p (con, args) =
    1.27      let
    1.28        val P_names = map P_name (1 upto (length dnames));
    1.29        val vns = Name.variant_list P_names (map vname args);
    1.30 @@ -367,7 +367,7 @@
    1.31    fun ind_prems_tac prems = EVERY
    1.32      (maps (fn cons =>
    1.33        (resolve_tac prems 1 ::
    1.34 -        maps (fn (_,_,args) => 
    1.35 +        maps (fn (_,args) => 
    1.36            resolve_tac prems 1 ::
    1.37            map (K(atac 1)) (nonlazy args) @
    1.38            map (K(atac 1)) (filter is_rec args))
    1.39 @@ -382,7 +382,7 @@
    1.40            ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
    1.41              rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
    1.42                (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
    1.43 -          ) o third) cons;
    1.44 +          ) o snd) cons;
    1.45      fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
    1.46      fun warn (n,cons) =
    1.47        if all_rec_to [] false (n,cons)
    1.48 @@ -414,7 +414,7 @@
    1.49                          (* FIXME! case_UU_tac *)
    1.50              case_UU_tac context (prems @ con_rews) 1
    1.51                (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
    1.52 -          fun con_tacs (con, _, args) = 
    1.53 +          fun con_tacs (con, args) = 
    1.54              asm_simp_tac take_ss 1 ::
    1.55              map arg_tac (filter is_nonlazy_rec args) @
    1.56              [resolve_tac prems 1] @
    1.57 @@ -490,7 +490,7 @@
    1.58                etac disjE 1,
    1.59                asm_simp_tac (HOL_ss addsimps con_rews) 1,
    1.60                asm_simp_tac take_ss 1];
    1.61 -            fun con_tacs ctxt (con, _, args) =
    1.62 +            fun con_tacs ctxt (con, args) =
    1.63                asm_simp_tac take_ss 1 ::
    1.64                maps (arg_tacs ctxt) (nonlazy_rec args);
    1.65              fun foo_tacs ctxt n (cons, cases) =