src/HOL/Tools/record.ML

   val empty = Symtab.make [tuple_iso_tuple];
   val extend = I;
   fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
 );
 
-fun get_typedef_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
-    { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
+fun get_typedef_info tyco vs
+    (({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy =
   let
     val exists_thm =
       UNIV_I
       |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
     val proj_constr = Abs_inverse OF [exists_thm];

 
 structure Record: RECORD =
 struct
 
 val eq_reflection = @{thm eq_reflection};
-val atomize_all = @{thm HOL.atomize_all};
-val atomize_imp = @{thm HOL.atomize_imp};
 val meta_allE = @{thm Pure.meta_allE};
 val prop_subst = @{thm prop_subst};
 val K_record_comp = @{thm K_record_comp};
 val K_comp_convs = [@{thm o_apply}, K_record_comp];
 val o_assoc = @{thm o_assoc};

 
 (** theory extender interface **)
 
 (* prepare arguments *)
 
-fun read_raw_parent ctxt raw_T =
-  (case ProofContext.read_typ_abbrev ctxt raw_T of
-    Type (name, Ts) => (Ts, name)
-  | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
-
 fun read_typ ctxt raw_T env =
   let
     val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
     val T = Syntax.read_typ ctxt' raw_T;
     val env' = OldTerm.add_typ_tfrees (T, env);