# HG changeset patch
# User wenzelm
# Date 1005920649 -3600
# Node ID cc31140bba168c763ea4092e5454271b24ecb3ad
# Parent  9dc4e8fec63dd9740abe21cfdea138ec4941574e
local_standard: plain strip_shyps instead of strip_shyps_warning;

diff -r 9dc4e8fec63d -r cc31140bba16 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Nov 16 13:48:43 2001 +0100
+++ b/src/Pure/drule.ML	Fri Nov 16 15:24:09 2001 +0100
@@ -374,7 +374,7 @@
 val standard = close_derivation o standard';
 
 fun local_standard th =
-  th |> strip_shyps_warning |> zero_var_indexes
+  th |> strip_shyps |> zero_var_indexes
   |> Thm.compress |> close_derivation;