src/HOL/Nominal/nominal_primrec.ML

     thy' |>
     ProofContext.init |>
     Proof.theorem_i NONE
       (fn thss => ProofContext.theory (fn thy =>
          let
-           val simps = flat thss;
+           val simps = map standard (flat thss);
            val (simps', thy') =
              fold_map note ((map fst eqns ~~ atts) ~~ map single simps) thy;
            val simps'' = maps snd simps'
          in
            thy'