--- a/src/Tools/IsaPlanner/rw_inst.ML Thu May 30 15:51:55 2013 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Thu May 30 16:11:14 2013 +0200
@@ -7,11 +7,6 @@
signature RW_INST =
sig
-
- val beta_eta_contract : thm -> thm
-
- (* Rewrite: give it instantiation infromation, a rule, and the
- target thm, and it will return the rewritten target thm *)
val rw : Proof.context ->
((indexname * (sort * typ)) list * (* type var instantiations *)
(indexname * (typ * term)) list) (* schematic var instantiations *)
@@ -28,15 +23,6 @@
structure RWInst : RW_INST =
struct
-
-(* beta-eta contract the theorem *)
-fun beta_eta_contract thm =
- let
- val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
- val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
- in thm3 end;
-
-
(* Given a list of variables that were bound, and a that has been
instantiated with free variable placeholders for the bound vars, it
creates an abstracted version of the theorem, with local bound vars as
@@ -234,7 +220,7 @@
rule_inst |> Thm.instantiate ([], cterm_renamings)
|> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
val specific_tgt_rule =
- beta_eta_contract
+ Conv.fconv_rule Drule.beta_eta_conversion
(Thm.combination couter_inst abstract_rule_inst);
(* create an instantiated version of the target thm *)
@@ -245,7 +231,7 @@
val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
in
- (beta_eta_contract tgt_th_inst)
+ Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst
|> Thm.equal_elim specific_tgt_rule
|> Drule.implies_intr_list cprems
|> Drule.forall_intr_list frees_of_fixed_vars
--- a/src/Tools/eqsubst.ML Thu May 30 15:51:55 2013 +0200
+++ b/src/Tools/eqsubst.ML Thu May 30 16:11:14 2013 +0200
@@ -247,7 +247,7 @@
fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
RWInst.rw ctxt m rule conclthm
|> IsaND.unfix_frees cfvs
- |> RWInst.beta_eta_contract
+ |> Conv.fconv_rule Drule.beta_eta_conversion
|> (fn r => Tactic.rtac r i st);
(* substitute within the conclusion of goal i of gth, using a meta
@@ -327,7 +327,7 @@
|> (Seq.hd o prune_params_tac)
|> Thm.permute_prems 0 ~1 (* put old asm first *)
|> IsaND.unfix_frees cfvs (* unfix any global params *)
- |> RWInst.beta_eta_contract; (* normal form *)
+ |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
in
(* ~j because new asm starts at back, thus we subtract 1 *)
Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))