diff --git a/src/ecScope.ml b/src/ecScope.ml
index d0125b46f..02cd1f57b 100644
--- a/src/ecScope.ml
+++ b/src/ecScope.ml
@@ -1435,8 +1435,8 @@ module Op = struct
     let add_distr_tag
         (pred : path) (bases : string list) (tag : string) (suffix : string) scope
     =
-      if not (EcAlgTactic.is_module_loaded (env scope)) then
-        hierror "for tag %s, load Distr first" tag;
+      if EcEnv.Op.by_path_opt pred (env scope) == None then
+         hierror "for tag %s, load Distr first" tag;
 
       let oppath   = EcPath.pqname (path scope) (unloc op.po_name) in
       let nparams  = List.map EcIdent.fresh tyop.op_tparams in
diff --git a/tests/rnd_ll.ec b/tests/rnd_ll.ec
new file mode 100644
index 000000000..53ce03f13
--- /dev/null
+++ b/tests/rnd_ll.ec
@@ -0,0 +1,19 @@
+require import AllCore.
+
+fail op[lossless] dC : bool distr.
+
+require import Distr.
+
+op[lossless] dC : bool distr.
+
+module M = { 
+  proc p1() = {
+    var e1;
+    e1 <$ dC;
+  }
+}.
+
+equiv foo : M.p1 ~ M.p1 : true ==> true.
+proc. 
+rnd.
+abort.
\ No newline at end of file
diff --git a/theories/crypto/DigitalSignatures.eca b/theories/crypto/DigitalSignatures.eca
index 1095dd7cc..a309433b5 100644
--- a/theories/crypto/DigitalSignatures.eca
+++ b/theories/crypto/DigitalSignatures.eca
@@ -12,7 +12,7 @@
 
 (* --- Require/Import Theories --- *)
 (* -- Built-in (i.e, standard library) -- *)
-require import AllCore List.
+require import AllCore List Distr.