src/Pure/Syntax/syntax.ML
changeset 27195 bbf4cbc69243
parent 26951 030e4a818b39
child 27265 49c81f6d7a08
--- a/src/Pure/Syntax/syntax.ML	Fri Jun 13 21:04:12 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Jun 13 21:04:42 2008 +0200
@@ -42,7 +42,7 @@
   val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
   val standard_parse_term: Pretty.pp -> (term -> string option) ->
     (((string * int) * sort) list -> string * int -> Term.sort) ->
-    (string -> string option) -> (string -> string option) ->
+    (string -> bool * string) -> (string -> string option) ->
     (typ -> typ) -> (sort -> sort) -> Proof.context ->
     (string -> bool) -> syntax -> typ -> string -> term
   val standard_parse_typ: Proof.context -> syntax ->