src/Pure/IsaPlanner/rw_inst.ML
changeset 18127 9f03d8a9a81b
parent 16179 fa7e70be26b0
     1.1 --- a/src/Pure/IsaPlanner/rw_inst.ML	Wed Nov 09 12:21:05 2005 +0100
     1.2 +++ b/src/Pure/IsaPlanner/rw_inst.ML	Wed Nov 09 16:26:41 2005 +0100
     1.3 @@ -296,8 +296,8 @@
     1.4          |> Drule.implies_intr_list cprems
     1.5          |> Drule.forall_intr_list frees_of_fixed_vars
     1.6          |> Drule.forall_elim_list vars
     1.7 -        |> fst o Thm.varifyT' othertfrees
     1.8 -        |> Drule.zero_var_indexes
     1.9 +        |> Thm.varifyT' othertfrees
    1.10 +        |-> K Drule.zero_var_indexes
    1.11      end;
    1.12  
    1.13