[Agda] operator treating

[Sergei Meshveliani]

Please, how to fix this for  Agda 2.4.3-candidate ?

--------------------------------------------------------------------
open import Algebra.FunctionProperties as FuncProp using (Op₂)
open import Relation.Binary.PropositionalEquality as PE using (_≢_)
open import Data.Nat using (ℕ; _*_)   

record Fr : Set where constructor fr′
                      field num   : ℕ
                            den   : ℕ
       	       	       	    den≉0 : den ≢ 0
infixl 7 _*fr_

_*fr_ : Op₂ Fr
(fr′ n d d≢0) *fr (foo′ n' d' d'≢0) =  fr′ (n * n') (d * d') dd'≢0
                               	       where
       	       	       	       	       postulate dd'≢0 :  d * d' ≢ 0
----------------------------------------------------------------------


The report is 

-------------------------------------- 
Could not parse the left-hand side
(fr′ n d d≢0) *fr (foo′ n' d' d'≢0)
Operators used in the grammar:
  *fr (infixl operator, level 7) [_*fr_
(/home/mechvel/doconA/0.04/source/demoTest/Operators.agda:20,1-6)]
(the treatment of operators has changed, so code that used to parse
may have to be changed)
when scope checking the left-hand side
(fr′ n d d≢0) *fr (foo′ n' d' d'≢0) in the definition of _*fr_
----------------------------------------

I copy the approach of  "  infixl 7 _*_  "
of  Data.Nat.
But it is not parsed.

Thank you in advance for explanation,

------
Sergei