# HG changeset patch
# User wenzelm
# Date 1216027183 -7200
# Node ID 6b20092af078d4c9d9f3dbef73297c10407abbc8
# Parent  4bb03d4509e2854565571bd749498b55236d886d
ProofNode.current

diff -r 4bb03d4509e2 -r 6b20092af078 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 _ =>