# 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 _ =>