src/HOL/Tools/choice_specification.ML
changeset 36954 ef698bd61057
parent 36945 9bec62c10714
child 36960 01594f816e3a
     1.1 --- a/src/HOL/Tools/choice_specification.ML	Sat May 15 23:40:00 2010 +0200
     1.2 +++ b/src/HOL/Tools/choice_specification.ML	Sun May 16 00:02:11 2010 +0200
     1.3 @@ -239,7 +239,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 Binding.name_of) -- P.prop)
     1.8 +          Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.command "specification" "define constants by specification" K.thy_goal
    1.12 @@ -250,7 +250,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 Binding.name_of) -- P.prop))
    1.17 +           Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
    1.18  
    1.19  val _ =
    1.20    OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal