src/Pure/General/scan.ML

--- a/src/Pure/General/scan.ML	Sat Oct 17 21:42:18 2015 +0200
+++ b/src/Pure/General/scan.ML	Sat Oct 17 22:31:21 2015 +0200
@@ -42,6 +42,8 @@
   val error: ('a -> 'b) -> 'a -> 'b
   val catch: ('a -> 'b) -> 'a -> 'b    (*exception Fail*)
   val recover: ('a -> 'b) -> (string -> 'a -> 'b) -> 'a -> 'b
+  val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
+  val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
   val fail: 'a -> 'b
   val fail_with: ('a -> message) -> 'a -> 'b
   val succeed: 'a -> 'b -> 'a * 'b
@@ -115,6 +117,12 @@
   catch scan1 xs handle Fail msg => scan2 msg xs;
 
 
+(* utils *)
+
+fun triple1 ((x, y), z) = (x, y, z);
+fun triple2 (x, (y, z)) = (x, y, z);
+
+
 (* scanner combinators *)
 
 fun (scan >> f) xs = scan xs |>> f;