qed_spec_mp: strip_shyps_warning;

--- a/src/HOL/HOL_lemmas.ML	Fri Jun 09 10:26:21 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML	Tue Jun 13 18:33:34 2000 +0200
@@ -529,7 +529,7 @@
 fun normalize_thm funs =
   let fun trans [] th = th
 	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
-  in zero_var_indexes o trans funs end;
+  in zero_var_indexes o strip_shyps_warning o trans funs end;
 
 fun qed_spec_mp name =
   let val thm = normalize_thm [RSspec,RSmp] (result())