diff -r 02eb07152998 -r 394870e51d18 src/HOL/Codatatype/Tools/bnf_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 11:51:07 2012 +0200
@@ -123,6 +123,7 @@
   val o_apply: thm
   val set_mp: thm
   val set_rev_mp: thm
+  val subset_UNIV: thm
   val Pair_eqD: thm
   val Pair_eqI: thm
   val mk_sym: thm -> thm
@@ -524,6 +525,7 @@
 val o_apply = @{thm o_apply};
 val set_mp = @{thm set_mp};
 val set_rev_mp = @{thm set_rev_mp};
+val subset_UNIV = @{thm subset_UNIV};
 val Pair_eqD = @{thm iffD1[OF Pair_eq]};
 val Pair_eqI = @{thm iffD2[OF Pair_eq]};