src/HOL/NatTransfer.thy

--- a/src/HOL/NatTransfer.thy	Tue Jul 21 14:38:07 2009 +0200
+++ b/src/HOL/NatTransfer.thy	Tue Jul 21 15:44:30 2009 +0200
@@ -380,12 +380,16 @@
     "(even (int x)) = (even x)"
   by (auto simp add: zdvd_int even_nat_def)
 
+lemma UNIV_apply:
+  "UNIV x = True"
+  by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq)
+
 declare TransferMorphism_int_nat[transfer add return:
   transfer_int_nat_numerals
   transfer_int_nat_functions
   transfer_int_nat_function_closures
   transfer_int_nat_relations
-  UNIV_code
+  UNIV_apply
 ]