src/Pure/tactic.ML
changeset 12498 3b0091bf06e8
parent 12320 6e70d870ddf0
child 12725 7ede865e1fe5
--- 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;