src/Pure/IsaPlanner/rw_inst.ML
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;