1.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sun Apr 25 00:10:30 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sun Apr 25 00:25:44 2010 +0200
     1.3 @@ -10,32 +10,32 @@
     1.4    type styp = Nitpick_Util.styp
     1.5    type hol_context = Nitpick_HOL.hol_context
     1.6  
     1.7 -  type constr_spec = {
     1.8 -    const: styp,
     1.9 -    delta: int,
    1.10 -    epsilon: int,
    1.11 -    exclusive: bool,
    1.12 -    explicit_max: int,
    1.13 -    total: bool}
    1.14 +  type constr_spec =
    1.15 +    {const: styp,
    1.16 +     delta: int,
    1.17 +     epsilon: int,
    1.18 +     exclusive: bool,
    1.19 +     explicit_max: int,
    1.20 +     total: bool}
    1.21  
    1.22 -  type dtype_spec = {
    1.23 -    typ: typ,
    1.24 -    card: int,
    1.25 -    co: bool,
    1.26 -    standard: bool,
    1.27 -    complete: bool * bool,
    1.28 -    concrete: bool * bool,
    1.29 -    deep: bool,
    1.30 -    constrs: constr_spec list}
    1.31 +  type dtype_spec =
    1.32 +    {typ: typ,
    1.33 +     card: int,
    1.34 +     co: bool,
    1.35 +     standard: bool,
    1.36 +     complete: bool * bool,
    1.37 +     concrete: bool * bool,
    1.38 +     deep: bool,
    1.39 +     constrs: constr_spec list}
    1.40  
    1.41 -  type scope = {
    1.42 -    hol_ctxt: hol_context,
    1.43 -    binarize: bool,
    1.44 -    card_assigns: (typ * int) list,
    1.45 -    bits: int,
    1.46 -    bisim_depth: int,
    1.47 -    datatypes: dtype_spec list,
    1.48 -    ofs: int Typtab.table}
    1.49 +  type scope =
    1.50 +    {hol_ctxt: hol_context,
    1.51 +     binarize: bool,
    1.52 +     card_assigns: (typ * int) list,
    1.53 +     bits: int,
    1.54 +     bisim_depth: int,
    1.55 +     datatypes: dtype_spec list,
    1.56 +     ofs: int Typtab.table}
    1.57  
    1.58    val datatype_spec : dtype_spec list -> typ -> dtype_spec option
    1.59    val constr_spec : dtype_spec list -> styp -> constr_spec
    1.60 @@ -61,32 +61,32 @@
    1.61  open Nitpick_Util
    1.62  open Nitpick_HOL
    1.63  
    1.64 -type constr_spec = {
    1.65 -  const: styp,
    1.66 -  delta: int,
    1.67 -  epsilon: int,
    1.68 -  exclusive: bool,
    1.69 -  explicit_max: int,
    1.70 -  total: bool}
    1.71 +type constr_spec =
    1.72 +  {const: styp,
    1.73 +   delta: int,
    1.74 +   epsilon: int,
    1.75 +   exclusive: bool,
    1.76 +   explicit_max: int,
    1.77 +   total: bool}
    1.78  
    1.79 -type dtype_spec = {
    1.80 -  typ: typ,
    1.81 -  card: int,
    1.82 -  co: bool,
    1.83 -  standard: bool,
    1.84 -  complete: bool * bool,
    1.85 -  concrete: bool * bool,
    1.86 -  deep: bool,
    1.87 -  constrs: constr_spec list}
    1.88 +type dtype_spec =
    1.89 +  {typ: typ,
    1.90 +   card: int,
    1.91 +   co: bool,
    1.92 +   standard: bool,
    1.93 +   complete: bool * bool,
    1.94 +   concrete: bool * bool,
    1.95 +   deep: bool,
    1.96 +   constrs: constr_spec list}
    1.97  
    1.98 -type scope = {
    1.99 -  hol_ctxt: hol_context,
   1.100 -  binarize: bool,
   1.101 -  card_assigns: (typ * int) list,
   1.102 -  bits: int,
   1.103 -  bisim_depth: int,
   1.104 -  datatypes: dtype_spec list,
   1.105 -  ofs: int Typtab.table}
   1.106 +type scope =
   1.107 +  {hol_ctxt: hol_context,
   1.108 +   binarize: bool,
   1.109 +   card_assigns: (typ * int) list,
   1.110 +   bits: int,
   1.111 +   bisim_depth: int,
   1.112 +   datatypes: dtype_spec list,
   1.113 +   ofs: int Typtab.table}
   1.114  
   1.115  datatype row_kind = Card of typ | Max of styp
   1.116