1.1 --- a/src/HOL/Tools/specification_package.ML	Fri Dec 05 18:42:39 2008 +0100
     1.2 +++ b/src/HOL/Tools/specification_package.ML	Fri Dec 05 18:43:42 2008 +0100
     1.3 @@ -233,7 +233,7 @@
     1.4  
     1.5  val specification_decl =
     1.6    P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
     1.7 -          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
     1.8 +          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.command "specification" "define constants by specification" K.thy_goal
    1.12 @@ -244,7 +244,7 @@
    1.13  val ax_specification_decl =
    1.14      P.name --
    1.15      (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
    1.16 -           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop))
    1.17 +           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop))
    1.18  
    1.19  val _ =
    1.20    OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal