More cleanup

Remove unused name schemes and DEF_kind

20 files changed, 89 insertions, 206 deletions

diff --git a/language/sail.ott b/language/sail.ott
index dfd9a423..0977d227 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -290,43 +290,6 @@ typschm :: 'TypSchm_' ::=
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 grammar
-%ctor_def :: 'CT_' ::=
-%  {{ com Datatype constructor definition clause }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
-%  | id : typschm                                       :: :: ct
-% but we could get away with disallowing constraints in typschm, we
-% think - if it's useful to do that
-
-%enum_opt :: 'EnumOpt_' ::=
-%  |      :: :: empty
-%  | enum :: :: enum
-
-%% tdefbody :: 'TD_' ::=
-%%   {{ com Type definition bodies }}
-%%   | typschm                                                     :: :: abbrev
-%%     {{ com Type abbreviations }}
-%%   | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |>     :: :: record
-%%     {{ com Record types }}
-%%   | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn            :: :: variant
-%%     {{ com Variant types }}
-%% 
- name_scm_opt :: 'Name_sect_' ::=
-   {{ com optional variable naming-scheme constraint}} 
-   {{ aux _ l }}
-   |                                                   :: :: none
-   | [ name = regexp ]                                 :: :: some
-%% 
-%% type_def :: '' ::=
-%%   {{ com Type definitions }}
-%%   | type id : kind naming_scheme_opt = tdefbody                                :: :: Td
-%% %  | enumeration id naming_scheme_opt = tdefbody                               ::   :: Td2
-%% % the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum...
-%% 
-
-% TODO: do we need mutually recursive type definitions?  
-
-
-%%% OR, IN C STYLE
 
 type_def {{ ocaml 'a type_def }} {{ lem type_def 'a }} :: 'TD_' ::=
   {{ ocaml TD_aux of type_def_aux * 'a annot }}
@@ -337,23 +300,15 @@ type_def_aux  :: 'TD_' ::=
   {{ com type definition body }}
   | type id typquant = typ_arg                                        :: :: abbrev
     {{ com type abbreviation }} {{ texlong }}
-  | typedef id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt }     :: :: record
+  | typedef id = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt }     :: :: record
     {{ com struct type definition }} {{ texlong }}
-  | typedef id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt }   :: :: variant
+  | typedef id = const union typquant { type_union1 ; ... ; type_unionn semi_opt }   :: :: variant
     {{ com tagged union type definition}} {{ texlong }}
-  | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
+  | typedef id = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
     {{ com enumeration type definition}} {{ texlong }}
   | bitfield id : typ = { id1 : index_range1 , ... , idn : index_rangen } :: :: bitfield
     {{ com register mutable bitfield type definition }} {{ texlong }}
 
-% the D(eprecated) forms here should be removed; they add complexity for no purpose.  The nexp abbreviation form should have better syntax.
-% ; many are shorthands for type\_defs
-kind_def :: 'KD_' ::=
-  {{ com Definition body for elements of kind }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | Def kind id name_scm_opt = nexp :: :: nabbrev
-    {{ com Int-expression abbreviation }}
-
 type_union :: 'Tu_' ::=
   {{ com type union constructors }}
   {{ aux _ l }}
@@ -924,7 +879,7 @@ scattered_def :: 'SD_' ::=
   | function clause funcl  :: :: funcl
 {{ texlong }} {{ com scattered function definition clause }}
 
-  | scattered typedef id name_scm_opt = const union typquant :: :: variant
+  | scattered typedef id = const union typquant :: :: variant
 {{ texlong }} {{ com scattered union definition header }}
 
   | union id member type_union :: :: unioncl
@@ -970,8 +925,6 @@ prec :: '' ::=
 def :: 'DEF_' ::=
   {{ com top-level definition }}
   {{ auxparam 'a }}
-  | kind_def                                           :: :: kind
-    {{ com definition of named kind identifiers }}
   | type_def                                           :: :: type
     {{ com type definition }}
   | fundef                                             :: :: fundef
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 36263615..b04a07e3 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -623,7 +623,6 @@ let exp_loc = function
   | E_aux (_, (l, _)) -> l
 
 let def_loc = function
-  | DEF_kind (KD_aux (_, (l, _)))
   | DEF_type (TD_aux (_, (l, _)))
   | DEF_fundef (FD_aux (_, (l, _)))
   | DEF_mapdef (MD_aux (_, (l, _)))
@@ -948,9 +947,9 @@ let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) =
 
 let id_of_type_def_aux = function
   | TD_abbrev (id, _, _)
-  | TD_record (id, _, _, _, _)
-  | TD_variant (id, _, _, _, _)
-  | TD_enum (id, _, _, _)
+  | TD_record (id, _, _, _)
+  | TD_variant (id, _, _, _)
+  | TD_enum (id, _, _)
   | TD_bitfield (id, _, _) -> id
 let id_of_type_def (TD_aux (td_aux, _)) = id_of_type_def_aux td_aux
 
@@ -964,7 +963,6 @@ let id_of_dec_spec (DEC_aux (ds_aux, _)) =
   | DEC_typ_alias (_, id, _) -> id
 
 let ids_of_def = function
-  | DEF_kind (KD_aux (KD_nabbrev (_, id, _, _), _)) -> IdSet.singleton id
   | DEF_type td -> IdSet.singleton (id_of_type_def td)
   | DEF_fundef fd -> IdSet.singleton (id_of_fundef fd)
   | DEF_val (LB_aux (LB_val (pat, _), _)) -> pat_ids pat
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 53e7dc88..458a5c45 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1390,16 +1390,16 @@ and compile_block ctx = function
    it returns a ctypdef * ctx pair. **)
 let compile_type_def ctx (TD_aux (type_def, _)) =
   match type_def with
-  | TD_enum (id, _, ids, _) ->
+  | TD_enum (id, ids, _) ->
      CTD_enum (id, ids),
      { ctx with enums = Bindings.add id (IdSet.of_list ids) ctx.enums }
 
-  | TD_record (id, _, _, ctors, _) ->
+  | TD_record (id, _, ctors, _) ->
      let ctors = List.fold_left (fun ctors (typ, id) -> Bindings.add id (ctyp_of_typ ctx typ) ctors) Bindings.empty ctors in
      CTD_struct (id, Bindings.bindings ctors),
      { ctx with records = Bindings.add id ctors ctx.records }
 
-  | TD_variant (id, _, _, tus, _) ->
+  | TD_variant (id, _, tus, _) ->
      let compile_tu = function
        | Tu_aux (Tu_ty_id (typ, id), _) -> ctyp_of_typ ctx typ, id
      in
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 16597b3a..99dd5f34 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -490,13 +490,6 @@ let to_ast_spec ctx (val_:P.val_spec) : (unit val_spec) ctx_out =
       let typschm, _ = to_ast_typschm ctx ts in
       VS_aux(VS_val_spec(typschm,to_ast_id id,ext,is_cast),(l,())),ctx)
 
-let to_ast_namescm (P.Name_sect_aux(ns,l)) =
-  Name_sect_aux(
-    (match ns with
-    | P.Name_sect_none -> Name_sect_none
-    | P.Name_sect_some(s) -> Name_sect_some(s)
-    ),l)
-
 let rec to_ast_range (P.BF_aux(r,l)) = (* TODO add check that ranges are sensible for some definition of sensible *)
   BF_aux(
     (match r with
@@ -523,24 +516,24 @@ let to_ast_typedef ctx (P.TD_aux (aux, l) : P.type_def) : unit type_def ctx_out
        TD_abbrev (id, typq, typ_arg),
        add_constructor id typq ctx
 
-    | P.TD_record (id, namescm_opt, typq, fields, _) ->
+    | P.TD_record (id, typq, fields, _) ->
        let id = to_ast_id id in
        let typq, typq_ctx = to_ast_typquant ctx typq in
        let fields = List.map (fun (atyp, id) -> to_ast_typ typq_ctx atyp, to_ast_id id) fields in
-       TD_record (id, to_ast_namescm namescm_opt, typq, fields, false),
+       TD_record (id, typq, fields, false),
        add_constructor id typq ctx
 
-    | P.TD_variant (id, namescm_opt, typq, arms, _) ->
+    | P.TD_variant (id, typq, arms, _) ->
        let id = to_ast_id id in
        let typq, typq_ctx = to_ast_typquant ctx typq in
        let arms = List.map (to_ast_type_union typq_ctx) arms in
-       TD_variant (id, to_ast_namescm namescm_opt, typq, arms, false),
+       TD_variant (id, typq, arms, false),
        add_constructor id typq ctx
 
-    | P.TD_enum (id, namescm_opt, enums, _) ->
+    | P.TD_enum (id, enums, _) ->
        let id = to_ast_id id in
        let enums = List.map to_ast_id enums in
-       TD_enum (id, to_ast_namescm namescm_opt, enums, false),
+       TD_enum (id, enums, false),
        { ctx with type_constructors = Bindings.add id [] ctx.type_constructors }
 
     | P.TD_bitfield (id, typ, ranges) ->
@@ -552,13 +545,6 @@ let to_ast_typedef ctx (P.TD_aux (aux, l) : P.type_def) : unit type_def ctx_out
   in
   TD_aux (aux, (l, ())), ctx
 
-let to_ast_kdef ctx (td:P.kind_def) : unit kind_def =
-  match td with
-  | P.KD_aux (P.KD_nabbrev (kind, id, name_scm_opt, atyp), l) ->
-     let id = to_ast_id id in
-     let kind = to_ast_kind kind in
-     KD_aux (KD_nabbrev (kind, id, to_ast_namescm name_scm_opt, to_ast_nexp ctx atyp), (l, ()))
-
 let to_ast_rec ctx (P.Rec_aux(r,l): P.rec_opt) : unit rec_opt =
   Rec_aux((match r with
   | P.Rec_nonrec -> Rec_nonrec
@@ -674,10 +660,10 @@ let to_ast_scattered ctx (P.SD_aux (aux, l)) =
        SD_function (to_ast_rec ctx rec_opt, tannot_opt, effect_opt, to_ast_id id), ctx
     | P.SD_funcl funcl ->
        SD_funcl (to_ast_funcl ctx funcl), ctx
-    | P.SD_variant (id, namescm_opt, typq) ->
+    | P.SD_variant (id, typq) ->
        let id = to_ast_id id in
        let typq, typq_ctx = to_ast_typquant ctx typq in
-       SD_variant (id, to_ast_namescm namescm_opt, typq),
+       SD_variant (id, typq),
        add_constructor id typq { ctx with scattereds = Bindings.add id typq_ctx ctx.scattereds }
     | P.SD_unioncl (id, tu) ->
        let id = to_ast_id id in
@@ -710,9 +696,6 @@ let to_ast_def ctx def : unit def ctx_out =
      DEF_overload (to_ast_id id, List.map to_ast_id ids), ctx
   | P.DEF_fixity (prec, n, op) ->
      DEF_fixity (to_ast_prec prec, n, to_ast_id op), ctx
-  | P.DEF_kind k_def ->
-     let kd = to_ast_kdef ctx k_def in
-     DEF_kind kd, ctx
   | P.DEF_type(t_def) ->
      let td, ctx = to_ast_typedef ctx t_def in
      DEF_type td, ctx
@@ -873,7 +856,7 @@ let generate_undefineds vs_ids (Defs defs) =
     | pats -> mk_pat (P_tup pats)
   in
   let undefined_td = function
-    | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
+    | TD_enum (id, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let typschm = typschm_of_string ("unit -> " ^ string_of_id id ^ " effect {undef}") in
        [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
@@ -883,13 +866,13 @@ let generate_undefineds vs_ids (Defs defs) =
                              else
                                mk_exp (E_app (mk_id "internal_pick",
                                               [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
-    | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
+    | TD_record (id, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in
        [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             pat
                             (mk_exp (E_record (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields)))]]
-    | TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
+    | TD_variant (id, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in
        let body =
          if !opt_fast_undefined && List.length tus > 0 then
@@ -967,7 +950,7 @@ let generate_initialize_registers vs_ids (Defs defs) =
 
 let generate_enum_functions vs_ids (Defs defs) =
   let rec gen_enums = function
-    | DEF_type (TD_aux (TD_enum (id, _, elems, _), _)) as enum :: defs ->
+    | DEF_type (TD_aux (TD_enum (id, elems, _), _)) as enum :: defs ->
        let enum_val_spec name quants typ =
          mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, (fun _ -> None), !opt_enum_casts))
        in
diff --git a/src/lexer.mll b/src/lexer.mll
index 57580e7a..55e765d9 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -146,7 +146,6 @@ let kw_table =
      ("return",                  (fun x -> Return));
      ("scattered",               (fun x -> Scattered));
      ("sizeof",                  (fun x -> Sizeof));
-     ("constant",                (fun x -> Constant));
      ("constraint",              (fun x -> Constraint));
      ("struct",                  (fun x -> Struct));
      ("then",                    (fun x -> Then));
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index eb50bac3..dbe0fafd 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -1192,9 +1192,9 @@ let split_defs all_errors splits defs =
     in
     let sc_type_def ((TD_aux (tda,annot)) as td) =
       match tda with
-      | TD_variant (id,nscm,quant,tus,flag) ->
+      | TD_variant (id,quant,tus,flag) ->
          let (refinements, tus') = List.split (List.map (sc_type_union quant) tus) in
-         (List.concat refinements, TD_aux (TD_variant (id,nscm,quant,List.concat tus',flag),annot))
+         (List.concat refinements, TD_aux (TD_variant (id,quant,List.concat tus',flag),annot))
       | _ -> ([],td)
     in
     let sc_def d =
@@ -2111,7 +2111,6 @@ let split_defs all_errors splits defs =
     in
     let map_def d =
       match d with
-      | DEF_kind _
       | DEF_type _
       | DEF_spec _
       | DEF_default _
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index ad2c198e..7f5f49e0 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -584,20 +584,20 @@ let ocaml_string_of_variant ctx id typq cases =
 
 let ocaml_typedef ctx (TD_aux (td_aux, _)) =
   match td_aux with
-  | TD_record (id, _, typq, fields, _) ->
+  | TD_record (id, typq, fields, _) ->
      ((separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals; lbrace]
        ^//^ ocaml_fields ctx fields)
       ^/^ rbrace)
      ^^ ocaml_def_end
      ^^ ocaml_string_of_struct ctx id typq fields
-  | TD_variant (id, _, _, cases, _) when string_of_id id = "exception" ->
+  | TD_variant (id, _, cases, _) when string_of_id id = "exception" ->
      ocaml_exceptions ctx cases
-  | TD_variant (id, _, typq, cases, _) ->
+  | TD_variant (id, typq, cases, _) ->
      (separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals]
       ^//^ ocaml_cases ctx cases)
      ^^ ocaml_def_end
      ^^ ocaml_string_of_variant ctx id typq cases
-  | TD_enum (id, _, ids, _) ->
+  | TD_enum (id, ids, _) ->
      (separate space [string "type"; zencode ctx id; equals]
       ^//^ (bar ^^ space ^^ ocaml_enum ctx ids))
      ^^ ocaml_def_end
@@ -708,9 +708,9 @@ let ocaml_pp_generators ctx defs orig_types required =
     match td with
     | TD_abbrev (_, _, A_aux (A_typ typ, _)) ->
        add_req_from_typ required typ
-    | TD_record (_, _, _, fields, _) ->
+    | TD_record (_, _, fields, _) ->
        List.fold_left (fun req (typ,_) -> add_req_from_typ req typ) required fields
-    | TD_variant (_, _, _, variants, _) ->
+    | TD_variant (_, _, variants, _) ->
        List.fold_left (fun req (Tu_aux (Tu_ty_id (typ,_),_)) ->
            add_req_from_typ req typ) required variants
     | TD_enum _ -> required
@@ -724,8 +724,8 @@ let ocaml_pp_generators ctx defs orig_types required =
       | TD_aux (td,_) ->
          (match td with
           | TD_abbrev (_,tqs,A_aux (A_typ _, _)) -> tqs
-          | TD_record (_,_,tqs,_,_) -> tqs
-          | TD_variant (_,_,tqs,_,_) -> tqs
+          | TD_record (_,tqs,_,_) -> tqs
+          | TD_variant (_,tqs,_,_) -> tqs
           | TD_enum _ -> TypQ_aux (TypQ_no_forall,Unknown)
           | TD_abbrev (_, _, _) -> assert false
           | TD_bitfield _ -> assert false)
@@ -847,7 +847,7 @@ let ocaml_pp_generators ctx defs orig_types required =
         match td with
         | TD_abbrev (_,tqs,A_aux (A_typ typ, _)) ->
            tqs, gen_type typ, None, None
-        | TD_variant (_,_,tqs,variants,_) ->
+        | TD_variant (_,tqs,variants,_) ->
            tqs,
            string "let c = rand_choice [" ^^ group (nest 2 (break 0 ^^
              separate_map (string ";" ^^ break 1) rand_variant variants) ^^
@@ -855,7 +855,7 @@ let ocaml_pp_generators ctx defs orig_types required =
              string "] in c g",
            Some (separate_map (string ";" ^^ break 1) variant_constructor variants),
            Some (separate_map (break 1) build_constructor variants)
-        | TD_enum (_,_,variants,_) ->
+        | TD_enum (_,variants,_) ->
            TypQ_aux (TypQ_no_forall, Parse_ast.Unknown),
            string "rand_choice [" ^^ group (nest 2 (break 0 ^^
              separate_map (string ";" ^^ break 1) (zencode_upper ctx) variants) ^^
@@ -863,7 +863,7 @@ let ocaml_pp_generators ctx defs orig_types required =
                string "]",
            Some (separate_map (string ";" ^^ break 1) enum_constructor variants),
            Some (separate_map (break 1) build_enum_constructor variants)
-        | TD_record (_,_,tqs,fields,_) ->
+        | TD_record (_,tqs,fields,_) ->
            tqs, braces (separate_map (string ";" ^^ break 1) rand_field fields), None, None
         | _ ->
            raise (Reporting.err_todo l "Generators for bitfields not yet supported")
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 65b11373..00da5afb 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -343,13 +343,6 @@ type_union_aux =  (* Type union constructors *)
    Tu_ty_id of atyp * id
  | Tu_ty_anon_rec of (atyp * id) list * id
 
-
-type 
-name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of string
-
-
 type 
 tannot_opt = 
    Typ_annot_opt_aux of tannot_opt_aux * l
@@ -383,12 +376,6 @@ index_range_aux =  (* index specification, for bitfields in register types *)
 and index_range = 
    BF_aux of index_range_aux * l
 
-
-type 
-name_scm_opt = 
-   Name_sect_aux of name_scm_opt_aux * l
-
-
 type 
 default_typing_spec_aux =  (* Default kinding or typing assumption, and default order for literal vectors and vector shorthands *)
    DT_order of kind * atyp
@@ -447,20 +434,15 @@ fundef_aux =  (* Function definition *)
 type 
 type_def_aux =  (* Type definition body *)
    TD_abbrev of id * typquant * kind * atyp (* type abbreviation *)
- | TD_record of id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
- | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
- | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *)
+ | TD_record of id * typquant * ((atyp * id)) list * bool (* struct type definition *)
+ | TD_variant of id * typquant * (type_union) list * bool (* union type definition *)
+ | TD_enum of id * (id) list * bool (* enumeration type definition *)
  | TD_bitfield of id * atyp * (id * index_range) list (* register mutable bitfield type definition *)
 
 type 
 val_spec_aux =  (* Value type specification *)
    VS_val_spec of typschm * id * (string -> string option) * bool
 
-
-type 
-kind_def_aux =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
-   KD_nabbrev of kind * id * name_scm_opt * atyp (* type abbreviation *)
-
 type 
 dec_spec_aux =  (* Register declarations *)
    DEC_reg of atyp * id
@@ -474,7 +456,7 @@ scattered_def_aux =  (* Function and type union definitions that can be spread a
          a file. Each one must end in $_$ *)
    SD_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
  | SD_funcl of funcl (* scattered function definition clause *)
- | SD_variant of id * name_scm_opt * typquant (* scattered union definition header *)
+ | SD_variant of id * typquant (* scattered union definition header *)
  | SD_unioncl of id * type_union (* scattered union definition member *)
  | SD_mapping of id * tannot_opt
  | SD_mapcl of id * mapcl
@@ -500,12 +482,6 @@ type
 val_spec = 
    VS_aux of val_spec_aux * l
 
-
-type 
-kind_def = 
-   KD_aux of kind_def_aux * l
-
-
 type 
 dec_spec = 
    DEC_aux of dec_spec_aux * l
@@ -521,8 +497,7 @@ type fixity_token = (prec * Big_int.num * string)
 
 type
 def =  (* Top-level definition *)
-   DEF_kind of kind_def (* definition of named kind identifiers *)
- | DEF_type of type_def (* type definition *)
+   DEF_type of type_def (* type definition *)
  | DEF_fundef of fundef (* function definition *)
  | DEF_mapdef of mapdef (* mapping definition *)
  | DEF_val of letbind (* value definition *)
diff --git a/src/parser.mly b/src/parser.mly
index 66902953..ef30991f 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -134,7 +134,6 @@ let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown))
 let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
 let mk_tannot typq typ n m = Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ), loc n m)
 let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown)
-let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown)
 
 let mk_typq kopts nc n m = TypQ_aux (TypQ_tq (List.map qi_id_of_kopt kopts @ nc), loc n m)
 
@@ -181,7 +180,7 @@ let rec desugar_rchain chain s e =
 %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op Where
 %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool Cast
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
-%token Undefined Union Newtype With Val Constant Constraint Throw Try Catch Exit Bitfield
+%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Mutual Var Ref Configuration
 
@@ -1170,21 +1169,21 @@ type_def:
   | Typedef id Colon kind Eq typ
     { mk_td (TD_abbrev ($2, mk_typqn, $4, $6)) $startpos $endpos }
   | Struct id Eq Lcurly struct_fields Rcurly
-    { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
+    { mk_td (TD_record ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
   | Struct id typaram Eq Lcurly struct_fields Rcurly
-    { mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+    { mk_td (TD_record ($2, $3, $6, false)) $startpos $endpos }
   | Enum id Eq enum_bar
-    { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos }
+    { mk_td (TD_enum ($2, $4, false)) $startpos $endpos }
   | Enum id Eq Lcurly enum Rcurly
-    { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos }
+    { mk_td (TD_enum ($2, $5, false)) $startpos $endpos }
   | Newtype id Eq type_union
-    { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos }
+    { mk_td (TD_variant ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos }
   | Newtype id typaram Eq type_union
-    { mk_td (TD_variant ($2, mk_namesectn, $3, [$5], false)) $startpos $endpos }
+    { mk_td (TD_variant ($2, $3, [$5], false)) $startpos $endpos }
   | Union id Eq Lcurly type_unions Rcurly
-    { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
+    { mk_td (TD_variant ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
   | Union id typaram Eq Lcurly type_unions Rcurly
-    { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+    { mk_td (TD_variant ($2, $3, $6, false)) $startpos $endpos }
   | Bitfield id Colon typ Eq Lcurly r_def_body Rcurly
     { mk_td (TD_bitfield ($2, $4, $7)) $startpos $endpos }
 
@@ -1375,9 +1374,9 @@ default_def:
 
 scattered_def:
   | Union id typaram
-    { mk_sd (SD_variant($2, mk_namesectn, $3)) $startpos $endpos }
+    { mk_sd (SD_variant($2, $3)) $startpos $endpos }
   | Union id
-    { mk_sd (SD_variant($2, mk_namesectn, mk_typqn)) $startpos $endpos }
+    { mk_sd (SD_variant($2, mk_typqn)) $startpos $endpos }
   | Function_ id
     { mk_sd (SD_function(mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos }
   | Mapping id
@@ -1423,9 +1422,6 @@ def:
     { DEF_scattered (mk_sd (SD_end $2) $startpos $endpos) }
   | default_def
     { DEF_default $1 }
-  | Constant id Eq typ
-    { DEF_kind (KD_aux (KD_nabbrev (K_aux (K_int, loc $startpos($1) $endpos($1)), $2, mk_namesectn, $4),
-			loc $startpos $endpos)) }
   | Mutual Lcurly fun_def_list Rcurly
     { DEF_internal_mutrec $3 }
   | Pragma
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index fa858eae..a8631886 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1720,7 +1720,6 @@ let types_used_with_generic_eq defs =
     fst (Rewriter.fold_pexp alg pexp)
   in
   let typs_req_def = function
-    | DEF_kind _
     | DEF_type _
     | DEF_spec _
     | DEF_fixity _
@@ -1758,7 +1757,7 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = match td with
                         doc_typquant_items empty_ctxt parens typq;
                         colon; string "Type"])
        (doc_typschm empty_ctxt false typschm) ^^ dot
-  | TD_record(id,nm,typq,fs,_) ->
+  | TD_record(id,typq,fs,_) ->
     let fname fid = if prefix_recordtype && string_of_id id <> "regstate"
                     then concat [doc_id id;string "_";doc_id_type fid;]
                     else doc_id_type fid in
@@ -1811,7 +1810,7 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = match td with
            (separate space [string "Record"; id_pp; doc_typquant_items empty_ctxt parens typq])
            ((*doc_typquant typq*) (braces (space ^^ align fs_doc ^^ space))) ^^
       dot ^^ hardline ^^ eq_pp ^^ updates_pp
-  | TD_variant(id,nm,typq,ar,_) ->
+  | TD_variant(id,typq,ar,_) ->
      (match id with
       | Id_aux ((Id "read_kind"),_) -> empty
       | Id_aux ((Id "write_kind"),_) -> empty
@@ -1835,7 +1834,7 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = match td with
             type, so undo that here. *)
          let resetimplicit = separate space [string "Arguments"; id_pp; colon; string "clear implicits."] in
          typ_pp ^^ dot ^^ hardline ^^ resetimplicit ^^ hardline ^^ hardline)
-  | TD_enum(id,nm,enums,_) ->
+  | TD_enum(id,enums,_) ->
      (match id with
       | Id_aux ((Id "read_kind"),_) -> empty
       | Id_aux ((Id "write_kind"),_) -> empty
@@ -2370,7 +2369,6 @@ let rec doc_def unimplemented generic_eq_types def =
   | DEF_val (LB_aux (LB_val (pat, exp), _)) -> doc_val pat exp
   | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point"
   | DEF_mapdef (MD_aux (_, (l,_))) -> unreachable l __POS__ "Coq doesn't support mappings"
-  | DEF_kind _ -> empty
   | DEF_pragma _ -> empty
 
 let find_exc_typ defs =
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 9281db31..6c0c3272 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1021,7 +1021,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
        (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
        (doc_typschm_lem false typschm)
   | TD_abbrev _ -> empty
-  | TD_record(id,nm,typq,fs,_) ->
+  | TD_record(id,typq,fs,_) ->
     let fname fid = if prefix_recordtype && string_of_id id <> "regstate"
                     then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
                     else doc_id_lem_type fid in
@@ -1073,7 +1073,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
            ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline
     (* if !opt_sequential && string_of_id id = "regstate" then empty
     else separate_map hardline doc_field fs *)
-  | TD_variant(id,nm,typq,ar,_) ->
+  | TD_variant(id,typq,ar,_) ->
      (match id with
       | Id_aux ((Id "read_kind"),_) -> empty
       | Id_aux ((Id "write_kind"),_) -> empty
@@ -1145,7 +1145,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
              fromInterpValuePP ^^ hardline ^^ hardline ^^
                fromToInterpValuePP ^^ hardline
            else empty)
-  | TD_enum(id,nm,enums,_) ->
+  | TD_enum(id,enums,_) ->
      (match id with
       | Id_aux ((Id "read_kind"),_) -> empty
       | Id_aux ((Id "write_kind"),_) -> empty
@@ -1428,7 +1428,6 @@ let rec doc_def_lem def =
      group (doc_let_lem empty_ctxt lbind) ^/^ hardline
   | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point"
 
-  | DEF_kind _ -> empty
   | DEF_mapdef (MD_aux (_, (l, _))) -> unreachable l __POS__ "Lem doesn't support mappings"
   | DEF_pragma _ -> empty
 
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 345312f7..df494036 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -594,16 +594,16 @@ let doc_typdef (TD_aux(td,_)) = match td with
        | None ->
           doc_op equals (concat [string "type"; space; doc_id id; doc_typ_arg_kind typ_arg]) (doc_typ_arg typ_arg)
      end
-  | TD_enum (id, _, ids, _) ->
+  | TD_enum (id, ids, _) ->
      separate space [string "enum"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
-  | TD_record (id, _, TypQ_aux (TypQ_no_forall, _), fields, _) | TD_record (id, _, TypQ_aux (TypQ_tq [], _), fields, _) ->
+  | TD_record (id, TypQ_aux (TypQ_no_forall, _), fields, _) | TD_record (id, TypQ_aux (TypQ_tq [], _), fields, _) ->
      separate space [string "struct"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace]
-  | TD_record (id, _, TypQ_aux (TypQ_tq qs, _), fields, _) ->
+  | TD_record (id, TypQ_aux (TypQ_tq qs, _), fields, _) ->
      separate space [string "struct"; doc_id id; doc_param_quants qs; equals;
                      surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace]
-  | TD_variant (id, _, TypQ_aux (TypQ_no_forall, _), unions, _) | TD_variant (id, _, TypQ_aux (TypQ_tq [], _), unions, _) ->
+  | TD_variant (id, TypQ_aux (TypQ_no_forall, _), unions, _) | TD_variant (id, TypQ_aux (TypQ_tq [], _), unions, _) ->
      separate space [string "union"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace]
-  | TD_variant (id, _, TypQ_aux (TypQ_tq qs, _), unions, _) ->
+  | TD_variant (id, TypQ_aux (TypQ_tq qs, _), unions, _) ->
      separate space [string "union"; doc_id id; doc_param_quants qs; equals;
                      surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace]
   | _ -> string "TYPEDEF"
@@ -631,9 +631,6 @@ let doc_prec = function
   | InfixL -> string "infixl"
   | InfixR -> string "infixr"
 
-let doc_kind_def (KD_aux (KD_nabbrev (_, id, _, nexp), _)) =
-  separate space [string "integer"; doc_id id; equals; doc_nexp nexp]
-
 let rec doc_scattered (SD_aux (sd_aux, _)) =
   match sd_aux with
   | SD_function (_, _, _, id) ->
@@ -642,9 +639,9 @@ let rec doc_scattered (SD_aux (sd_aux, _)) =
      string "function" ^^ space ^^ string "clause" ^^ space ^^ doc_funcl funcl
   | SD_end id ->
      string "end" ^^ space ^^ doc_id id
-  | SD_variant (id, _, TypQ_aux (TypQ_no_forall, _)) ->
+  | SD_variant (id, TypQ_aux (TypQ_no_forall, _)) ->
      string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id
-  | SD_variant (id, _, TypQ_aux (TypQ_tq quants, _)) ->
+  | SD_variant (id, TypQ_aux (TypQ_tq quants, _)) ->
      string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id ^^ doc_param_quants quants
   | SD_unioncl (id, tu) ->
      separate space [string "union clause"; doc_id id; equals; doc_union tu]
@@ -653,7 +650,6 @@ let rec doc_def def = group (match def with
   | DEF_default df -> doc_default df
   | DEF_spec v_spec -> doc_spec v_spec
   | DEF_type t_def -> doc_typdef t_def
-  | DEF_kind k_def -> doc_kind_def k_def
   | DEF_fundef f_def -> doc_fundef f_def
   | DEF_mapdef m_def -> doc_mapdef m_def
   | DEF_val lbind -> string "let" ^^ space ^^ doc_letbind lbind
diff --git a/src/process_file.ml b/src/process_file.ml
index 03fc36a2..12f2b7c0 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -126,7 +126,7 @@ let parseid_to_string (Parse_ast.Id_aux (id, _)) =
 
 let rec realise_union_anon_rec_types orig_union arms =
   match orig_union with
-  | Parse_ast.TD_variant (union_id, name_scm_opt, typq, _, flag) ->
+  | Parse_ast.TD_variant (union_id, typq, _, flag) ->
      begin match arms with
      | [] -> []
      | arm :: arms ->
@@ -137,7 +137,7 @@ let rec realise_union_anon_rec_types orig_union arms =
            let record_str = "_" ^ parseid_to_string union_id ^ "_" ^ parseid_to_string id ^ "_record" in
            let record_id = Id_aux (Id record_str, Generated l) in
            let new_arm = Tu_aux ((Tu_ty_id ((ATyp_aux (ATyp_id record_id, Generated l)), id)), Generated l) in
-           let new_rec_def = DEF_type (TD_aux (TD_record (record_id, name_scm_opt, typq, fields, flag), Generated l)) in
+           let new_rec_def = DEF_type (TD_aux (TD_record (record_id, typq, fields, flag), Generated l)) in
            (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms)
      end
   | _ ->
@@ -210,7 +210,7 @@ let rec preprocess opts = function
 
   (* realise any anonymous record arms of variants *)
   | Parse_ast.DEF_type (Parse_ast.TD_aux
-                          (Parse_ast.TD_variant (id, name_scm_opt, typq, arms, flag) as union, l)
+                          (Parse_ast.TD_variant (id, typq, arms, flag) as union, l)
                        ) :: defs ->
      let records_and_arms = realise_union_anon_rec_types union arms in
      let rec filter_records = function [] -> []
@@ -219,7 +219,7 @@ let rec preprocess opts = function
      in
      let generated_records = filter_records (List.map fst records_and_arms) in
      let rewritten_arms = List.map snd records_and_arms in
-     let rewritten_union = Parse_ast.TD_variant (id, name_scm_opt, typq, rewritten_arms, flag) in
+     let rewritten_union = Parse_ast.TD_variant (id, typq, rewritten_arms, flag) in
      generated_records @ (Parse_ast.DEF_type (Parse_ast.TD_aux (rewritten_union, l))) :: preprocess opts defs
 
   | (Parse_ast.DEF_default (Parse_ast.DT_aux (Parse_ast.DT_order (_, Parse_ast.ATyp_aux (atyp, _)), _)) as def) :: defs ->
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 330a98f6..ae19e447 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -358,7 +358,7 @@ let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls
 let rewrite_def rewriters d = match d with
   | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), annot)) ->
      DEF_reg_dec (DEC_aux (DEC_config (id, typ, rewriters.rewrite_exp rewriters exp), annot))
-  | DEF_type _ | DEF_mapdef _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_overload _ | DEF_fixity _ -> d
+  | DEF_type _ | DEF_mapdef _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_overload _ | DEF_fixity _ -> d
   | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef)
   | DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs)
   | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 16efcd55..9f082f49 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2307,11 +2307,11 @@ let rewrite_type_def_typs rw_typ rw_typquant (TD_aux (td, annot)) =
   match td with
   | TD_abbrev (id, typq, A_aux (A_typ typ, l)) ->
      TD_aux (TD_abbrev (id, rw_typquant typq, A_aux (A_typ (rw_typ typ), l)), annot)
-  | TD_record (id, nso, typq, typ_ids, flag) ->
-     TD_aux (TD_record (id, nso, rw_typquant typq, List.map (fun (typ, id) -> (rw_typ typ, id)) typ_ids, flag), annot)
-  | TD_variant (id, nso, typq, tus, flag) ->
-     TD_aux (TD_variant (id, nso, rw_typquant typq, List.map (rewrite_type_union_typs rw_typ) tus, flag), annot)
-  | TD_enum (id, nso, ids, flag) -> TD_aux (TD_enum (id, nso, ids, flag), annot)
+  | TD_record (id, typq, typ_ids, flag) ->
+     TD_aux (TD_record (id, rw_typquant typq, List.map (fun (typ, id) -> (rw_typ typ, id)) typ_ids, flag), annot)
+  | TD_variant (id, typq, tus, flag) ->
+     TD_aux (TD_variant (id, rw_typquant typq, List.map (rewrite_type_union_typs rw_typ) tus, flag), annot)
+  | TD_enum (id, ids, flag) -> TD_aux (TD_enum (id, ids, flag), annot)
   | TD_bitfield _ -> assert false (* Processed before re-writing *)
 
 (* FIXME: other reg_dec types *)
diff --git a/src/scattered.ml b/src/scattered.ml
index be304dc8..de286e3f 100644
--- a/src/scattered.ml
+++ b/src/scattered.ml
@@ -126,9 +126,9 @@ let rec descatter' funcls mapcls = function
   (* For scattered unions, when we find a union declaration we
      immediately grab all the future clauses and turn it into a
      regular union declaration. *)
-  | DEF_scattered (SD_aux (SD_variant (id, namescm, typq), (l, _))) :: defs ->
+  | DEF_scattered (SD_aux (SD_variant (id, typq), (l, _))) :: defs ->
      let tus = get_union_clauses id defs in
-     DEF_type (TD_aux (TD_variant (id, namescm, typq, tus, false), (gen_loc l, Type_check.empty_tannot)))
+     DEF_type (TD_aux (TD_variant (id, typq, tus, false), (gen_loc l, Type_check.empty_tannot)))
      :: descatter' funcls mapcls (filter_union_clauses id defs)
 
   (* Therefore we should never see SD_unioncl... *)
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 88e80dd2..c7b93dbe 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -306,9 +306,6 @@ let typ_variants consider_var bound tunions =
     tunions
     (bound,mt)
 
-let fv_of_kind_def consider_var (KD_aux(k,_)) = match k with
-  | KD_nabbrev(_,id,_,nexp) -> init_env (string_of_id id), fv_of_nexp consider_var mt mt nexp
-
 let fv_of_abbrev consider_var bound used typq typ_arg =
   let ts_bound = if consider_var then typq_bindings typq else mt in
   ts_bound, fv_of_targ consider_var (Nameset.union bound ts_bound) used typ_arg
@@ -316,14 +313,14 @@ let fv_of_abbrev consider_var bound used typq typ_arg =
 let fv_of_type_def consider_var (TD_aux(t,_)) = match t with
   | TD_abbrev(id,typq,typ_arg) ->
      init_env (string_of_id id), snd (fv_of_abbrev consider_var mt mt typq typ_arg)
-  | TD_record(id,_,typq,tids,_) ->
+  | TD_record(id,typq,tids,_) ->
     let binds = init_env (string_of_id id) in
     let bounds = if consider_var then typq_bindings typq else mt in
     binds, List.fold_right (fun (t,_) n -> fv_of_typ consider_var bounds n t) tids mt
-  | TD_variant(id,_,typq,tunions,_) ->
+  | TD_variant(id,typq,tunions,_) ->
     let bindings = Nameset.add (string_of_id id) (if consider_var then typq_bindings typq else mt) in
     typ_variants consider_var bindings tunions
-  | TD_enum(id,_,ids,_) ->
+  | TD_enum(id,ids,_) ->
     Nameset.of_list (List.map string_of_id (id::ids)),mt
   | TD_bitfield(id,typ,_) ->
     init_env (string_of_id id), Nameset.empty (* fv_of_typ consider_var mt typ *)
@@ -429,7 +426,7 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd
             | _ -> mt in
           scattered_binds, exp_ns
      end
-  | SD_variant (id,_,_) ->
+  | SD_variant (id,_) ->
     let name = string_of_id id in
     let uses =
       if consider_scatter_as_one
@@ -480,7 +477,6 @@ let fv_of_rd consider_var (DEC_aux (d, annot)) =
      init_env (string_of_id id), mt
 
 let fv_of_def consider_var consider_scatter_as_one all_defs = function
-  | DEF_kind kdef -> fv_of_kind_def consider_var kdef
   | DEF_type tdef -> fv_of_type_def consider_var tdef
   | DEF_fundef fdef -> fv_of_fun consider_var fdef
   | DEF_mapdef mdef -> mt,mt (* fv_of_map consider_var mdef *)
diff --git a/src/specialize.ml b/src/specialize.ml
index 1881de5b..b619edde 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -171,7 +171,7 @@ let id_of_instantiation id instantiation =
 
 let rec variant_generic_typ id (Defs defs) =
   match defs with
-  | DEF_type (TD_aux (TD_variant (id', _, typq, _, _), _)) :: _ when Id.compare id id' = 0 ->
+  | DEF_type (TD_aux (TD_variant (id', typq, _, _), _)) :: _ when Id.compare id id' = 0 ->
      mk_typ (Typ_app (id', List.map (fun kopt -> mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt))))) (quant_kopts typq)))
   | _ :: defs -> variant_generic_typ id (Defs defs)
   | [] -> failwith ("No variant with id " ^ string_of_id id)
diff --git a/src/state.ml b/src/state.ml
index c9a47b06..63a07c0e 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -136,10 +136,10 @@ let generate_initial_regstate defs =
       List.fold_left2 typ_subst_quant_item typ (quant_items tq) args
     in
     let add_typ_init_val vals = function
-      | TD_enum (id, _, id1 :: _, _) ->
+      | TD_enum (id, id1 :: _, _) ->
          (* Choose the first value of an enumeration type as default *)
          Bindings.add id (fun _ -> string_of_id id1) vals
-      | TD_variant (id, _, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) ->
+      | TD_variant (id, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) ->
          (* Choose the first variant of a union type as default *)
          let init_val args =
            let typ1 = typ_subst_typquant tq args typ1 in
@@ -149,7 +149,7 @@ let generate_initial_regstate defs =
       | TD_abbrev (id, tq, A_aux (A_typ typ, _)) ->
          let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in
          Bindings.add id init_val vals
-      | TD_record (id, _, tq, fields, _) ->
+      | TD_record (id, tq, fields, _) ->
          let init_val args =
            let init_field (typ, id) =
              let typ = typ_subst_typquant tq args typ in
diff --git a/src/type_check.ml b/src/type_check.ml
index ad9fab34..b891f4c7 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -4483,30 +4483,22 @@ let mk_synonym typq typ_arg =
                                       ^ " in type synonym " ^ string_of_typ_arg typ_arg
                                       ^ " with " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
 
-let check_kinddef env (KD_aux (kdef, (l, _))) =
-  let kd_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented kind def") in
-  match kdef with
-  | KD_nabbrev (K_aux (K_int, _) as kind, id, nmscm, nexp) ->
-     [DEF_kind (KD_aux (KD_nabbrev (kind, id, nmscm, nexp), (l, None)))],
-     Env.add_num_def id nexp env
-  | _ -> kd_err ()
-
 let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
   fun env (TD_aux (tdef, (l, _))) ->
   let td_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Typedef") in
   match tdef with
   | TD_abbrev (id, typq, typ_arg) ->
      [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ_arg) env
-  | TD_record (id, nmscm, typq, fields, _) ->
+  | TD_record (id, typq, fields, _) ->
      [DEF_type (TD_aux (tdef, (l, None)))], Env.add_record id typq fields env
-  | TD_variant (id, nmscm, typq, arms, _) ->
+  | TD_variant (id, typq, arms, _) ->
      let env =
        env
        |> Env.add_variant id (typq, arms)
        |> (fun env -> List.fold_left (fun env tu -> check_type_union env id typq tu) env arms)
      in
      [DEF_type (TD_aux (tdef, (l, None)))], env
-  | TD_enum (id, nmscm, ids, _) ->
+  | TD_enum (id, ids, _) ->
      [DEF_type (TD_aux (tdef, (l, None)))], Env.add_enum id ids env
   | TD_bitfield (id, typ, ranges) ->
      let typ = Env.expand_synonyms env typ in
@@ -4528,8 +4520,8 @@ and check_scattered : 'a. Env.t -> 'a scattered_def -> (tannot def) list * Env.t
   fun env (SD_aux (sdef, (l, _))) ->
   match sdef with
   | SD_function _ | SD_end _ | SD_mapping _ -> [], env
-  | SD_variant (id, namescm, typq) ->
-     [DEF_scattered (SD_aux (SD_variant (id, namescm, typq), (l, None)))], Env.add_scattered_variant id typq env
+  | SD_variant (id, typq) ->
+     [DEF_scattered (SD_aux (SD_variant (id, typq), (l, None)))], Env.add_scattered_variant id typq env
   | SD_unioncl (id, tu) ->
      [DEF_scattered (SD_aux (SD_unioncl (id, tu), (l, None)))],
      let env = Env.add_variant_clause id tu env in
@@ -4550,7 +4542,6 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
   fun env def ->
   let cd_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Case") in
   match def with
-  | DEF_kind kdef -> check_kinddef env kdef
   | DEF_type tdef -> check_typedef env tdef
   | DEF_fixity (prec, n, op) -> [DEF_fixity (prec, n, op)], env
   | DEF_fundef fdef -> check_fundef env fdef