src/HOL/Tools/specification_package.ML
changeset 22101 6d13239d5f52
parent 21858 05f57309170c
child 22578 b0eb5652f210
--- a/src/HOL/Tools/specification_package.ML	Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOL/Tools/specification_package.ML	Fri Jan 19 22:08:08 2007 +0100
@@ -241,7 +241,7 @@
 
 val specification_decl =
   P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-          Scan.repeat1 (P.opt_thm_name ":" -- P.prop)
+          Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
 
 val specificationP =
   OuterSyntax.command "specification" "define constants by specification" K.thy_goal
@@ -252,7 +252,7 @@
 val ax_specification_decl =
     P.name --
     (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-           Scan.repeat1 (P.opt_thm_name ":" -- P.prop))
+           Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
 
 val ax_specificationP =
   OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal