--- 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)})
--- 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
--- 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 = "?"