# HG changeset patch
# User wenzelm
# Date 1256763635 -3600
# Node ID 0f99569d23e108e04fc2a89231f6a1e9c68a6811
# Parent  1807921b6268062878e527c9198f04645b3b8a66
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;

diff -r 1807921b6268 -r 0f99569d23e1 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Oct 28 20:49:09 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Oct 28 22:00:35 2009 +0100
@@ -222,22 +222,13 @@
 
 (* constant definitions and abbreviations *)
 
-val constdecl =
-  P.binding --
-    (P.where_ >> K (NONE, NoSyn) ||
-      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
-      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
-  >> P.triple2;
-
-val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
-
 val _ =
   OuterSyntax.local_theory "definition" "constant definition" K.thy_decl
-    (constdef >> (fn args => #2 o Specification.definition_cmd args));
+    (SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args));
 
 val _ =
   OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl
-    (opt_mode -- (Scan.option constdecl -- P.prop)
+    (opt_mode -- (Scan.option SpecParse.constdecl -- P.prop)
     >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
 
 val _ =
diff -r 1807921b6268 -r 0f99569d23e1 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Wed Oct 28 20:49:09 2009 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Wed Oct 28 22:00:35 2009 +0100
@@ -18,6 +18,8 @@
   val xthm: (Facts.ref * Attrib.src list) parser
   val xthms1: (Facts.ref * Attrib.src list) list parser
   val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
+  val constdecl: (binding * string option * mixfix) parser
+  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
   val locale_mixfix: mixfix parser
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
@@ -66,6 +68,18 @@
 val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
 
 
+(* basic constant specifications *)
+
+val constdecl =
+  P.binding --
+    (P.where_ >> K (NONE, NoSyn) ||
+      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
+      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
+  >> P.triple2;
+
+val constdef = Scan.option constdecl -- (opt_thm_name ":" -- P.prop);
+
+
 (* locale and context elements *)
 
 val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;