src/Pure/drule.ML
changeset 14391 bb726050650d
parent 14387 e96d5c42c4b0
child 14394 51b24127eef2
     1.1 --- a/src/Pure/drule.ML	Tue Feb 17 10:41:59 2004 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Feb 17 17:41:30 2004 +0100
     1.3 @@ -384,13 +384,13 @@
     1.4  fun standard' th =
     1.5    let val {maxidx,...} = rep_thm th in
     1.6      th
     1.7 -    |> flexflex_unique |> implies_intr_hyps 
     1.8 +    |> implies_intr_hyps
     1.9      |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
    1.10      |> strip_shyps_warning
    1.11      |> zero_var_indexes |> Thm.varifyT |> Thm.compress
    1.12    end;
    1.13  
    1.14 -val standard = close_derivation o standard';
    1.15 +val standard = close_derivation o standard' o flexflex_unique;
    1.16  
    1.17  fun local_standard th =
    1.18    th |> strip_shyps |> zero_var_indexes