diff --git a/HB/common/database.elpi b/HB/common/database.elpi
index 73091efa5..2b0268daa 100644
--- a/HB/common/database.elpi
+++ b/HB/common/database.elpi
@@ -67,13 +67,6 @@ extract-builder (builder-decl B) B.
 pred leq-builder i:builder, i:builder.
 leq-builder (builder N _ _ _) (builder M _ _ _) :- N =< M.
 
-% [factory-alias->gref X GR] when X is already a factory X = GR
-% however, when X is a phantom abbreviated gref, we find the underlying
-% factory gref GR associated to it.
-pred factory-alias->gref i:gref, o:gref.
-factory-alias->gref PhGR GR :- phant-abbrev GR PhGR _, !.
-factory-alias->gref GR GR :- phant-abbrev GR _ _, !.
-
 pred sub-class? i:class, i:class.
 sub-class? (class C1 _ ML1P) (class C2 _ ML2P) :-
   not (C1 = C2),
diff --git a/structures.v b/structures.v
index 5a8a81e02..8b2bf7b5e 100644
--- a/structures.v
+++ b/structures.v
@@ -126,6 +126,13 @@ pred from o:factoryname, o:mixinname, o:gref.
 %      Notation   Abbrev t1 := (AbbrevCst t1 _ idfun).
 pred phant-abbrev o:gref, o:gref, o:abbreviation.
 
+% [factory-alias->gref X GR] when X is already a factory X = GR
+% however, when X is a phantom abbreviated gref, we find the underlying
+% factory gref GR associated to it.
+pred factory-alias->gref i:gref, o:gref.
+factory-alias->gref PhGR GR :- phant-abbrev GR PhGR _, !.
+factory-alias->gref GR GR :- phant-abbrev GR _ _, !.
+
 %%%%% Cache of known facts %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % [factory-constructor F K] means K is a constructor for