# HG changeset patch
# User wenzelm
# Date 1213631688 -7200
# Node ID e60cdbc5e8e1a1878a696d72b0a1b26b6d40c5d2
# Parent  224c830e7abe3f4c7dc9679d395f27114de1e8e2
export eof;

diff -r 224c830e7abe -r e60cdbc5e8e1 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Jun 16 17:54:47 2008 +0200
+++ b/src/Pure/Isar/args.ML	Mon Jun 16 17:54:48 2008 +0200
@@ -22,6 +22,7 @@
   val mk_term: term -> T
   val mk_fact: thm list -> T
   val mk_attribute: (morphism -> attribute) -> T
+  val eof: T
   val stopper: T * (T -> bool)
   val not_eof: T -> bool
   type src