# HG changeset patch
# User wenzelm
# Date 896367721 -7200
# Node ID 2c567fcdb36d7ecfadab075f7a5fefb79cbaa60d
# Parent  6f96354267e0810fbb84421df64636b14fa0bf8b
changed get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option;

diff -r 6f96354267e0 -r 2c567fcdb36d src/Pure/Syntax/source.ML
--- a/src/Pure/Syntax/source.ML	Thu May 28 14:50:40 1998 +0200
+++ b/src/Pure/Syntax/source.ML	Thu May 28 17:02:01 1998 +0200
@@ -11,7 +11,7 @@
   val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source
   val get: ('a, 'b) source -> 'a list * ('a, 'b) source
   val unget: 'a list * ('a, 'b) source -> ('a, 'b) source
-  val get_single: ('a, 'b) source -> 'a option * ('a, 'b) source
+  val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option
   val exhaust: ('a, 'b) source -> 'a list
   val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
   val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
@@ -70,8 +70,8 @@
 
 fun get_single src =
   (case get src of
-    ([], src') => (None, src')
-  | (x :: xs, src') => (Some x, unget (xs, src')));
+    ([], _) => None
+  | (x :: xs, src') => Some (x, unget (xs, src')));
 
 fun exhaust src =
   (case get src of