# HG changeset patch
# User blanchet
# Date 1236178179 -3600
# Node ID 63cae7fd7e64232f3b5b9d2ede1730888cd8bcbd
# Parent  35518956f0ee091e2762517c398df8af62b225fc
Fix parentheses.

diff -r 35518956f0ee -r 63cae7fd7e64 src/HOL/Nominal/nominal_primrec.ML
--- 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] |>