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;