From 1ada99f2c367c2b2bad39377c38c4dc6e4b5a04a Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 23 Jul 2014 16:11:08 +0200
Subject: Derive plugin: small refactoring.

---
 plugins/Derive/derive.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml
index bf4b78b048..fbf7131e67 100644
--- a/plugins/Derive/derive.ml
+++ b/plugins/Derive/derive.ml
@@ -55,19 +55,18 @@ let start_deriving f suchthat lemma =
         let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in
         let f_kn = Declare.declare_constant f f_def in
         let f_kn_term = Term.mkConst f_kn in
+        let substf c = Vars.replace_vars [f,f_kn_term] c in
         let lemma_pretype =
           match Entries.(lemma_def.const_entry_type) with
           | Some t -> t
           | None -> assert false (* Proof_global always sets type here. *)
         in
         (* substitutes the variable [f] by the constant [f] it was standing for. *)
-        let lemma_type = Vars.replace_vars [f,f_kn_term] lemma_pretype in
+        let lemma_type = substf lemma_pretype in
         (* The type of [lemma_def] is adjusted to refer to [f_kn], the
            opacity is adjusted by the proof ending command.  *)
         let lemma_body =
-          map_const_entry_body begin fun c ->
-            Vars.replace_vars [f,f_kn_term] c
-          end Entries.(lemma_def.const_entry_body)
+          map_const_entry_body substf Entries.(lemma_def.const_entry_body)
         in
         let lemma_def = let open Entries in { lemma_def with
           const_entry_body = lemma_body ;
-- 
cgit v1.2.3