diff -r d64545e6cba5 -r bb3a5fa94a91 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Mon Nov 02 20:50:48 2009 +0100
+++ b/src/Pure/Isar/element.ML	Mon Nov 02 20:57:48 2009 +0100
@@ -294,7 +294,7 @@
 fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
   gen_witness_proof (fn after_qed' => fn propss =>
     Proof.map_context (K goal_ctxt)
-    #> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
+    #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
       cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
     (fn wits => fn _ => after_qed wits) wit_propss [];