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;