remove redundant function arguments
authorhuffman
Mon Mar 08 12:43:44 2010 -0800 (2010-03-08)
changeset 356608169419cd824
parent 35659 a78bc1930a7a
child 35661 ede27eb8e94b
remove redundant function arguments
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 12:36:26 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 12:43:44 2010 -0800
     1.3 @@ -208,8 +208,6 @@
     1.4  
     1.5  fun prove_induction
     1.6      (comp_dnam, eqs : eq list)
     1.7 -    (take_lemmas : thm list)
     1.8 -    (axs_reach : thm list)
     1.9      (take_rews : thm list)
    1.10      (take_info : Domain_Take_Proofs.take_induct_info)
    1.11      (thy : theory) =
    1.12 @@ -232,7 +230,7 @@
    1.13    end;
    1.14  
    1.15    val {take_0_thms, take_Suc_thms, chain_take_thms, ...} = take_info;
    1.16 -  val {lub_take_thms, finite_defs, ...} = take_info;
    1.17 +  val {lub_take_thms, finite_defs, reach_thms, ...} = take_info;
    1.18  
    1.19    fun one_con p (con, args) =
    1.20      let
    1.21 @@ -410,7 +408,7 @@
    1.22                  EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems];
    1.23              val subthm = Goal.prove context [] [] subgoal' (K subtac);
    1.24            in
    1.25 -            map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
    1.26 +            map (fn ax_reach => rtac (ax_reach RS subst) 1) reach_thms @ [
    1.27              cut_facts_tac (subthm :: take (length dnames) prems) 1,
    1.28              REPEAT (rtac @{thm conjI} 1 ORELSE
    1.29                      EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1,
    1.30 @@ -636,7 +634,6 @@
    1.31  (* theorems about take *)
    1.32  
    1.33  val take_lemmas = #take_lemma_thms take_info;
    1.34 -val axs_reach = #reach_thms take_info;
    1.35  
    1.36  val take_rews =
    1.37      maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
    1.38 @@ -644,7 +641,7 @@
    1.39  (* prove induction rules, unless definition is indirect recursive *)
    1.40  val thy =
    1.41      if is_indirect then thy else
    1.42 -    prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews take_info thy;
    1.43 +    prove_induction (comp_dnam, eqs) take_rews take_info thy;
    1.44  
    1.45  val thy =
    1.46      if is_indirect then thy else