# HG changeset patch
# User blanchet
# Date 1272148406 -7200
# Node ID 8f81c060cf12b4baf0f9853851a274ebb2629184
# Parent  eee4ee6a5cbe55906f68f7d5fda8aa806d382434
cosmetics

diff -r eee4ee6a5cbe -r 8f81c060cf12 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 25 00:25:44 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 25 00:33:26 2010 +0200
@@ -264,7 +264,7 @@
   val empty = {frac_types = [], codatatypes = []}
   val extend = I
   fun merge ({frac_types = fs1, codatatypes = cs1},
-               {frac_types = fs2, codatatypes = cs2}) : T =
+             {frac_types = fs2, codatatypes = cs2}) : T =
     {frac_types = AList.merge (op =) (K true) (fs1, fs2),
      codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
 
diff -r eee4ee6a5cbe -r 8f81c060cf12 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Apr 25 00:25:44 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Apr 25 00:33:26 2010 +0200
@@ -128,9 +128,9 @@
 
 structure Data = Theory_Data(
   type T = raw_param list
-  val empty = default_default_params |> map (apsnd single)
+  val empty = map (apsnd single) default_default_params
   val extend = I
-  fun merge p : T = AList.merge (op =) (K true) p)
+  val merge = AList.merge (op =) (K true))
 
 val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
 val default_raw_params = Data.get
diff -r eee4ee6a5cbe -r 8f81c060cf12 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 25 00:25:44 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 25 00:33:26 2010 +0200
@@ -62,7 +62,7 @@
   type T = (typ * term_postprocessor) list
   val empty = []
   val extend = I
-  fun merge (ps1, ps2) = AList.merge (op =) (K true) (ps1, ps2))
+  val merge = AList.merge (op =) (K true))
 
 val irrelevant = "_"
 val unknown = "?"