src/HOL/Tools/primrec_package.ML

 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
 val primrec_decl =
   Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" --
-    Scan.repeat1 (P.opt_thm_name ":" -- P.term);
+    Scan.repeat1 (P.opt_thm_name ":" -- P.term --| P.marg_comment);
 
 val primrecP =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
     (primrec_decl >> (fn (alt_name, eqns) =>
       Toplevel.theory (#1 o add_primrec alt_name (map P.triple_swap eqns))));