qed_spec_mp is a mess;

--- a/src/HOL/HOL_lemmas.ML	Tue Oct 19 13:45:51 1999 +0200
+++ b/src/HOL/HOL_lemmas.ML	Tue Oct 19 16:23:46 1999 +0200
@@ -452,6 +452,8 @@
 
 (** strip ! and --> from proved goal while preserving !-bound var names **)
 
+(** THIS CODE IS A MESS!!! **)
+
 local
 
 (* Use XXX to avoid forall_intr failing because of duplicate variable name *)