author huffman Mon Mar 08 12:43:44 2010 -0800 (2010-03-08) changeset 35660 8169419cd824 parent 35659 a78bc1930a7a child 35661 ede27eb8e94b
remove redundant function arguments
```     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
```