diff -r 8e46cf4fe26c -r a928e3439067 src/Pure/Isar/proof_node.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/proof_node.ML	Mon Jul 14 11:19:38 2008 +0200
@@ -0,0 +1,52 @@
+(*  Title:      Pure/Isar/proof_node.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Proof nodes with linear position and backtracking.
+*)
+
+signature PROOF_NODE =
+sig
+  type T
+  val init: Proof.state -> T
+  val current: T -> Proof.state
+  val position: T -> int
+  val back: T -> T
+  val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
+  val apply: (Proof.state -> Proof.state) -> T -> T
+end;
+
+structure ProofNode: PROOF_NODE =
+struct
+
+(* datatype *)
+
+datatype T = ProofNode of
+  (Proof.state *                (*first result*)
+   Proof.state Seq.seq) *       (*alternative results*)
+  int;                          (*linear proof position*)
+
+fun init st = ProofNode ((st, Seq.empty), 0);
+
+fun current (ProofNode ((st, _), _)) = st;
+fun position (ProofNode (_, n)) = n;
+
+
+(* backtracking *)
+
+fun back (ProofNode ((_, stq), n)) =
+  (case Seq.pull stq of
+    NONE => error "back: no alternatives"
+  | SOME res => ProofNode (res, n));
+
+
+(* apply transformer *)
+
+fun applys f (ProofNode (node as (st, _), n)) =
+  (case Seq.pull (f st) of
+    NONE => error "empty result sequence -- proof command failed"
+  | SOME res => ProofNode (res, n + 1));
+
+fun apply f = applys (Seq.single o f);
+
+end;