adapted Toplevel.Proof;
authorwenzelm
Wed Jan 04 00:52:42 2006 +0100 (2006-01-04)
changeset 185606b4570eb22d2
parent 18559 05b3f033c72d
child 18561 b0e134637479
adapted Toplevel.Proof;
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Wed Jan 04 00:52:40 2006 +0100
     1.2 +++ b/src/Pure/proof_general.ML	Wed Jan 04 00:52:42 2006 +0100
     1.3 @@ -1197,7 +1197,7 @@
     1.4    end
     1.5  
     1.6    val topnode = Toplevel.node_of o Toplevel.get_state
     1.7 -  fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph)
     1.8 +  fun topproofpos () = (case topnode() of Toplevel.Proof (h, _) => SOME(ProofHistory.position h)
     1.9                                          | _ => NONE) handle Toplevel.UNDEF => NONE
    1.10  in
    1.11