src/HOL/Nominal/nominal_primrec.ML

            |> snd
          end)
       [goals] |>
     Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
       rewrite_goals_tac defs_thms THEN
-      compose_tac (false, rule, length rule_prems) 1), Position.none)) |>
+      compose_tac (false, rule, length rule_prems) 1)) |>
     Seq.hd
   end;
 
 in