cosmetics
authorblanchet
Sun Apr 25 00:33:26 2010 +0200 (2010-04-25)
changeset 363918f81c060cf12
parent 36390 eee4ee6a5cbe
child 36392 c00c57850eb7
cosmetics
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 25 00:25:44 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 25 00:33:26 2010 +0200
     1.3 @@ -264,7 +264,7 @@
     1.4    val empty = {frac_types = [], codatatypes = []}
     1.5    val extend = I
     1.6    fun merge ({frac_types = fs1, codatatypes = cs1},
     1.7 -               {frac_types = fs2, codatatypes = cs2}) : T =
     1.8 +             {frac_types = fs2, codatatypes = cs2}) : T =
     1.9      {frac_types = AList.merge (op =) (K true) (fs1, fs2),
    1.10       codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
    1.11  
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Apr 25 00:25:44 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Apr 25 00:33:26 2010 +0200
     2.3 @@ -128,9 +128,9 @@
     2.4  
     2.5  structure Data = Theory_Data(
     2.6    type T = raw_param list
     2.7 -  val empty = default_default_params |> map (apsnd single)
     2.8 +  val empty = map (apsnd single) default_default_params
     2.9    val extend = I
    2.10 -  fun merge p : T = AList.merge (op =) (K true) p)
    2.11 +  val merge = AList.merge (op =) (K true))
    2.12  
    2.13  val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
    2.14  val default_raw_params = Data.get
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 25 00:25:44 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 25 00:33:26 2010 +0200
     3.3 @@ -62,7 +62,7 @@
     3.4    type T = (typ * term_postprocessor) list
     3.5    val empty = []
     3.6    val extend = I
     3.7 -  fun merge (ps1, ps2) = AList.merge (op =) (K true) (ps1, ps2))
     3.8 +  val merge = AList.merge (op =) (K true))
     3.9  
    3.10  val irrelevant = "_"
    3.11  val unknown = "?"