# HG changeset patch # User berghofe # Date 1014222646 -3600 # Node ID f5bceeec9d91f642ac39549639272852d82b0303 # Parent d3ad295a087a2d3f731c469ce38d8a3fc38b8d3d Removed superfluous lookup of theorems in Relation.thy diff -r d3ad295a087a -r f5bceeec9d91 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Feb 20 16:13:58 2002 +0100 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Feb 20 17:30:46 2002 +0100 @@ -100,8 +100,6 @@ val _ = message "Constructing primrec combinators ..."; val fun_rel_comp_name = "Relation.fun_rel_comp"; - val [fun_rel_comp_def, o_def] = - map (get_thm Relation.thy) ["fun_rel_comp_def", "o_def"]; val big_name = space_implode "_" new_type_names; val thy0 = add_path flat_names big_name thy;