--- a/src/HOL/Tools/record.ML Sat Jan 15 14:56:57 2011 +0100
+++ b/src/HOL/Tools/record.ML Sat Jan 15 15:29:17 2011 +0100
@@ -93,8 +93,8 @@
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
@@ -196,8 +196,6 @@
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};
@@ -1509,11 +1507,6 @@
(* 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;