Removed superfluous lookup of theorems in Relation.thy
authorberghofe
Wed, 20 Feb 2002 17:30:46 +0100
changeset 12910 f5bceeec9d91
parent 12909 d3ad295a087a
child 12911 704713ca07ea
Removed superfluous lookup of theorems in Relation.thy
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;