# HG changeset patch
# User wenzelm
# Date 1254342385 -7200
# Node ID 4271aab3aa4acb967518b12fec3dd9dc107a83bf
# Parent  f1ac4b515af9c421bb86dfcb896bac564e1cd8db
actually export unit parser;

diff -r f1ac4b515af9 -r 4271aab3aa4a src/Pure/Isar/value_parse.ML
--- a/src/Pure/Isar/value_parse.ML	Wed Sep 30 22:25:50 2009 +0200
+++ b/src/Pure/Isar/value_parse.ML	Wed Sep 30 22:26:25 2009 +0200
@@ -9,6 +9,7 @@
   val comma: 'a parser -> 'a parser
   val equal: 'a parser -> 'a parser
   val parens: 'a parser -> 'a parser
+  val unit: unit parser
   val pair: 'a parser -> 'b parser -> ('a * 'b) parser
   val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
   val list: 'a parser -> 'a list parser