author | berghofe |
Wed, 20 Feb 2002 17:30:46 +0100 | |
changeset 12910 | f5bceeec9d91 |
parent 12909 | d3ad295a087a |
child 12911 | 704713ca07ea |
--- 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;