author | blanchet |
Wed, 04 Mar 2009 15:49:39 +0100 | |
changeset 30253 | 63cae7fd7e64 |
parent 30252 | 35518956f0ee |
child 30254 | 7b8afdfa2f83 |
--- a/src/HOL/Nominal/nominal_primrec.ML Wed Mar 04 15:33:07 2009 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Wed Mar 04 15:49:39 2009 +0100 @@ -374,9 +374,9 @@ in lthy'' |> LocalTheory.note Thm.theoremK ((qualify (Binding.name "simps"), - (map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add], - maps snd simps') + map (Attrib.internal o K) + [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]), + maps snd simps') |> snd end) [goals] |>