From 466c25ea43149deedf50e0105a6d1e69db91c8fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Sep 2014 17:58:12 +0200
Subject: Removing the old implementation of clear_body.

---
 plugins/decl_mode/decl_proof_instr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 8f20cea6be..b5566127f1 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -222,7 +222,7 @@ let add_justification_hyps keep items gls =
 	  let id=pf_get_new_id local_hyp_prefix gls in
 	    keep:=Id.Set.add id !keep;
 	    tclTHEN (Proofview.V82.of_tactic (letin_tac None (Names.Name id) c None Locusops.nowhere))
-              (thin_body [id]) gls in
+              (Proofview.V82.of_tactic (clear_body [id])) gls in
     tclMAP add_aux items gls
 
 let prepare_goal items gls =
-- 
cgit v1.2.3