diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index bc8331ad3c9efd8c9fa18a649cf7e98f0ff840a8..a2ce1c72e39a2115017d7b4a0619014144b8abe7 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2239,8 +2239,10 @@ struct
     let fresh sigma t = fresh sigma.pool t
 
     let call f e =
-      let v = f e in
-      validate "Qed.Subst.add_fun" v ; v
+      if lc_closed e then
+        let v = f e in
+        validate "Qed.Subst.add_fun" v ; v
+      else raise Not_found
 
     let rec compute e = function
       | EMPTY -> raise Not_found