src/Pure/tactic.ML
changeset 12498 3b0091bf06e8
parent 12320 6e70d870ddf0
child 12725 7ede865e1fe5
     1.1 --- a/src/Pure/tactic.ML	Fri Dec 14 11:52:32 2001 +0100
     1.2 +++ b/src/Pure/tactic.ML	Fri Dec 14 11:52:54 2001 +0100
     1.3 @@ -662,7 +662,7 @@
     1.4        |> Drule.implies_intr_list casms
     1.5        |> Drule.forall_intr_list cparams
     1.6        |> norm_hhf
     1.7 -      |> Thm.varifyT' fixed_tfrees
     1.8 +      |> (#1 o Thm.varifyT' fixed_tfrees)
     1.9        |> Drule.zero_var_indexes
    1.10    end;
    1.11