diff -r 02eb07152998 -r 394870e51d18 src/HOL/Codatatype/Tools/bnf_comp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 11:51:07 2012 +0200
@@ -56,7 +56,6 @@
 val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
 val ordIso_transitive = @{thm ordIso_transitive};
 val ordLeq_csum2 = @{thm ordLeq_csum2};
-val subset_UNIV = @{thm subset_UNIV};
 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
 val trans_o_apply = @{thm trans[OF o_apply]};