# 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;