src/HOL/Tools/specification_package.ML

 val opt_name = Scan.optional (P.name --| P.$$$ ":") ""
 val opt_overloaded = P.opt_keyword "overloaded";
 
 val specification_decl =
   P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-          Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
+          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
 
 val _ =
   OuterSyntax.command "specification" "define constants by specification" K.thy_goal
     (specification_decl >> (fn (cos,alt_props) =>
                                Toplevel.print o (Toplevel.theory_to_proof
                                                      (process_spec NONE cos alt_props))))
 
 val ax_specification_decl =
     P.name --
     (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-           Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
+           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop))
 
 val _ =
   OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
     (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
                                Toplevel.print o (Toplevel.theory_to_proof