diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 7a2a8774a2879c799d600886d122348bdcbe1fcd..cd515a64e8735ba82f96359f68c18ce041d5b2ab 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -884,7 +884,7 @@ struct
 
   let c_record fxs =
     match fxs with
-    | [] | [_] -> insert(Rdef fxs)
+    | [] -> insert(Rdef fxs)
     | fx::gys ->
         try
           let base (f,v) =
@@ -2550,7 +2550,8 @@ struct
                | _ -> true)
             fvs
         in
-        Some ( base , fothers )
+        if fothers = [] then None (* suspiscious *)
+        else Some ( base , fothers )
 
   (* ------------------------------------------------------------------------ *)
   (* ---  Symbol                                                          --- *)