diff -r 5f54721547a7 -r eb4343a0d571 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Sep 28 10:44:51 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 28 13:54:49 2004 +0200
@@ -878,14 +878,6 @@
       (case kind of Theorem x => x | _ => err_malformed "finish_global" state);
 
     val ts = flat tss;
-val _ = set show_hyps;
-val _ = PolyML.print "finish_global";
-val _ = PolyML.print "ts:";
-val _ = PolyML.print ts;
-val _ = PolyML.print "raw_thm:";
-val _ = PolyML.print raw_thm;
-val _ = PolyML.print "elems_view";
-val _ = PolyML.print elems_view;
     val locale_results = map (ProofContext.export_standard elems_view goal_ctxt locale_ctxt)
       (prep_result state ts raw_thm);