# HG changeset patch
# User wenzelm
# Date 1236457164 -3600
# Node ID 3fc32dd7a64721c8a60438cd87f5e75426eeb8be
# Parent  51d488f3dd7200972385c4de6fb624cc990a24f5
added const_binding;

diff -r 51d488f3dd72 -r 3fc32dd7a647 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Sat Mar 07 21:18:37 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Sat Mar 07 21:19:24 2009 +0100
@@ -81,6 +81,7 @@
   val opt_mixfix': mixfix parser
   val where_: string parser
   val const: (string * string * mixfix) parser
+  val const_binding: (binding * string * mixfix) parser
   val params: (binding * string option) list parser
   val simple_fixes: (binding * string option) list parser
   val fixes: (binding * string option * mixfix) list parser
@@ -291,6 +292,7 @@
 val where_ = $$$ "where";
 
 val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
+val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
 
 val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
   >> (fn (xs, T) => map (rpair T) xs);