# 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