local_standard: plain strip_shyps instead of strip_shyps_warning;
authorwenzelm
Fri, 16 Nov 2001 15:24:09 +0100
changeset 12221 cc31140bba16
parent 12220 9dc4e8fec63d
child 12222 d1c276b45dbc
local_standard: plain strip_shyps instead of strip_shyps_warning;
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;