diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/parse.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -6,8 +6,6 @@
 
 signature PARSE =
 sig
-  type 'a parser = Token.T list -> 'a * Token.T list
-  type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
   val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
   val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
   val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
@@ -114,10 +112,6 @@
 structure Parse: PARSE =
 struct
 
-type 'a parser = Token.T list -> 'a * Token.T list;
-type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list);
-
-
 (** error handling **)
 
 (* group atomic parsers (no cuts!) *)
@@ -441,6 +435,3 @@
 
 end;
 
-type 'a parser = 'a Parse.parser;
-type 'a context_parser = 'a Parse.context_parser;
-