src/Pure/Isar/proof_context.ML

         val tfrees = gen (Term.add_term_tfree_names (prop, []));
       in
         rule
         |> Drule.forall_intr_list frees
         |> Goal.norm_hhf
-        |> (#1 o Drule.tvars_intr_list tfrees)
+        |> Drule.tvars_intr_list tfrees |> #2
       end)
   end;
 
 fun export inner outer =
   let val exp = common_exports false inner outer in