ProofNode.current
authorwenzelm
Mon Jul 14 11:19:43 2008 +0200 (2008-07-14)
changeset 275666b20092af078
parent 27565 4bb03d4509e2
child 27567 e3fe9a327c63
ProofNode.current
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Jul 14 11:19:42 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Jul 14 11:19:43 2008 +0200
     1.3 @@ -497,7 +497,7 @@
     1.4  
     1.5  fun proof_state node =
     1.6    (case Option.map Toplevel.proof_node node of
     1.7 -    SOME (SOME prf) => ProofHistory.current prf
     1.8 +    SOME (SOME prf) => ProofNode.current prf
     1.9    | _ => error "No proof state");
    1.10  
    1.11  fun output_goals main_goal src node = args (Scan.succeed ()) (output (fn _ => fn _ =>