changeset 31902 | 862ae16a799d |
parent 31723 | f5cafe803b55 |
child 31938 | f193d95b4632 |
--- a/src/HOL/Nominal/nominal_primrec.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Thu Jul 02 17:34:14 2009 +0200 @@ -373,7 +373,7 @@ lthy'' |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"), map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]), + [Simplifier.simp_add, Nitpick_Const_Simps.add]), maps snd simps') |> snd end)