# HG changeset patch
# User wenzelm
# Date 960914014 -7200
# Node ID 7856a01119fb91a1e3f97a953add1029589d0b63
# Parent  af1ca1acf292f127f5e7afc0eb81fd05f4fc72a1
qed_spec_mp: strip_shyps_warning;

diff -r af1ca1acf292 -r 7856a01119fb src/HOL/HOL_lemmas.ML
--- 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())