src/Pure/Isar/isar_syn.ML

 
 (* arbitrary overloading *)
 
 val _ =
   OuterSyntax.command "overloading" "overloaded definitions" K.thy_decl
-   (Scan.repeat1 (P.xname --| P.$$$ "::" -- P.typ --| P.$$$ "is" -- P.name --
+   (Scan.repeat1 (P.name --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term --
       Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true)
         --| P.begin
    >> (fn operations => Toplevel.print o
          Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations)));