# HG changeset patch
# User wenzelm
# Date 1008327174 -3600
# Node ID 3b0091bf06e857225ddcc8ea04981a1d5fa63f80
# Parent  ec6ba9e6eef389fcd508a36947cbd5a99137f7bb
changed Thm.varifyT';

diff -r ec6ba9e6eef3 -r 3b0091bf06e8 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Dec 14 11:52:32 2001 +0100
+++ b/src/Pure/tactic.ML	Fri Dec 14 11:52:54 2001 +0100
@@ -662,7 +662,7 @@
       |> Drule.implies_intr_list casms
       |> Drule.forall_intr_list cparams
       |> norm_hhf
-      |> Thm.varifyT' fixed_tfrees
+      |> (#1 o Thm.varifyT' fixed_tfrees)
       |> Drule.zero_var_indexes
   end;