local_standard: plain strip_shyps instead of strip_shyps_warning;
authorwenzelm
Fri Nov 16 15:24:09 2001 +0100 (2001-11-16)
changeset 12221cc31140bba16
parent 12220 9dc4e8fec63d
child 12222 d1c276b45dbc
local_standard: plain strip_shyps instead of strip_shyps_warning;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Fri Nov 16 13:48:43 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Nov 16 15:24:09 2001 +0100
     1.3 @@ -374,7 +374,7 @@
     1.4  val standard = close_derivation o standard';
     1.5  
     1.6  fun local_standard th =
     1.7 -  th |> strip_shyps_warning |> zero_var_indexes
     1.8 +  th |> strip_shyps |> zero_var_indexes
     1.9    |> Thm.compress |> close_derivation;
    1.10  
    1.11