Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/specification_package.ML
changeset 29006 abe0f11cfa4e
parent 28083 103d9282a946
child 29265 5b4247055bd7 
--- a/src/HOL/Tools/specification_package.ML	Fri Dec 05 18:42:39 2008 +0100
+++ b/src/HOL/Tools/specification_package.ML	Fri Dec 05 18:43:42 2008 +0100
@@ -233,7 +233,7 @@
 
 val specification_decl =
   P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
+          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
 
 val _ =
   OuterSyntax.command "specification" "define constants by specification" K.thy_goal
@@ -244,7 +244,7 @@
 val ax_specification_decl =
     P.name --
     (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop))
+           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop))
 
 val _ =
   OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
isabelle