author | wenzelm |
Fri, 16 Nov 2001 15:24:09 +0100 | |
changeset 12221 | cc31140bba16 |
parent 12220 | 9dc4e8fec63d |
child 12222 | d1c276b45dbc |
src/Pure/drule.ML | file | annotate | diff | comparison | revisions |
--- 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;