src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 41472 f6ab14e61604
parent 41052 3db267a01c1d
child 41791 01d722707a36
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 08 16:01:51 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 08 17:14:48 2011 +0100
     1.3 @@ -275,7 +275,8 @@
     1.4  datatype boxability =
     1.5    InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
     1.6  
     1.7 -structure Data = Generic_Data(
     1.8 +structure Data = Generic_Data
     1.9 +(
    1.10    type T = {frac_types: (string * (string * string) list) list,
    1.11              codatatypes: (string * (string * styp list)) list}
    1.12    val empty = {frac_types = [], codatatypes = []}
    1.13 @@ -283,7 +284,8 @@
    1.14    fun merge ({frac_types = fs1, codatatypes = cs1},
    1.15               {frac_types = fs2, codatatypes = cs2}) : T =
    1.16      {frac_types = AList.merge (op =) (K true) (fs1, fs2),
    1.17 -     codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
    1.18 +     codatatypes = AList.merge (op =) (K true) (cs1, cs2)}
    1.19 +)
    1.20  
    1.21  val name_sep = "$"
    1.22  val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep