src/Pure/conjunction.ML
changeset 35985 0bbf0d2348f9
parent 35845 e5980f0ad025
child 43329 84472e198515
     1.1 --- a/src/Pure/conjunction.ML	Sat Mar 27 14:10:37 2010 +0100
     1.2 +++ b/src/Pure/conjunction.ML	Sat Mar 27 15:20:31 2010 +0100
     1.3 @@ -137,7 +137,7 @@
     1.4  
     1.5  fun comp_rule th rule =
     1.6    Thm.adjust_maxidx_thm ~1 (th COMP
     1.7 -    (rule |> Drule.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
     1.8 +    (rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
     1.9  
    1.10  in
    1.11