changeset 21618 | 1cbb1134cb6c |
parent 21541 | ea881fbe0489 |
child 21767 | 78ed5e22766a |
--- a/src/HOL/Nominal/nominal_primrec.ML Fri Dec 01 12:23:53 2006 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Fri Dec 01 16:08:45 2006 +0100 @@ -354,7 +354,7 @@ 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'