1.1 --- a/src/Pure/Isar/proof_node.ML	Mon Nov 02 20:57:48 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_node.ML	Mon Nov 02 21:03:41 2009 +0100
     1.3 @@ -15,36 +15,36 @@
     1.4    val apply: (Proof.state -> Proof.state) -> T -> T
     1.5  end;
     1.6  
     1.7 -structure ProofNode: PROOF_NODE =
     1.8 +structure Proof_Node: PROOF_NODE =
     1.9  struct
    1.10  
    1.11  (* datatype *)
    1.12  
    1.13 -datatype T = ProofNode of
    1.14 +datatype T = Proof_Node of
    1.15    (Proof.state *                (*first result*)
    1.16     Proof.state Seq.seq) *       (*alternative results*)
    1.17    int;                          (*linear proof position*)
    1.18  
    1.19 -fun init st = ProofNode ((st, Seq.empty), 0);
    1.20 +fun init st = Proof_Node ((st, Seq.empty), 0);
    1.21  
    1.22 -fun current (ProofNode ((st, _), _)) = st;
    1.23 -fun position (ProofNode (_, n)) = n;
    1.24 +fun current (Proof_Node ((st, _), _)) = st;
    1.25 +fun position (Proof_Node (_, n)) = n;
    1.26  
    1.27  
    1.28  (* backtracking *)
    1.29  
    1.30 -fun back (ProofNode ((_, stq), n)) =
    1.31 +fun back (Proof_Node ((_, stq), n)) =
    1.32    (case Seq.pull stq of
    1.33      NONE => error "back: no alternatives"
    1.34 -  | SOME res => ProofNode (res, n));
    1.35 +  | SOME res => Proof_Node (res, n));
    1.36  
    1.37  
    1.38  (* apply transformer *)
    1.39  
    1.40 -fun applys f (ProofNode ((st, _), n)) =
    1.41 +fun applys f (Proof_Node ((st, _), n)) =
    1.42    (case Seq.pull (f st) of
    1.43      NONE => error "empty result sequence -- proof command failed"
    1.44 -  | SOME res => ProofNode (res, n + 1));
    1.45 +  | SOME res => Proof_Node (res, n + 1));
    1.46  
    1.47  fun apply f = applys (Seq.single o f);
    1.48