--- a/src/HOL/IOA/NTP/Correctness.ML Fri Nov 17 13:22:50 1995 +0100
+++ b/src/HOL/IOA/NTP/Correctness.ML Fri Nov 17 15:10:36 1995 +0100
@@ -117,4 +117,4 @@
by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
by(Asm_full_simp_tac 1);
-result();
+qed"ntp_correct";