# HG changeset patch
# User wenzelm
# Date 1369923074 -7200
# Node ID 6a6033fa507c2174a46d8d7e9eb50a397586b69e
# Parent  d84ff5a93764f6a60c7ab13b8b83250193af297e
prefer existing beta_eta_conversion;

diff -r d84ff5a93764 -r 6a6033fa507c src/Tools/IsaPlanner/rw_inst.ML
--- 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
diff -r d84ff5a93764 -r 6a6033fa507c src/Tools/eqsubst.ML
--- 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))