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