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