diff -r 5c5bb83f2bae -r 1ea89d2a1bd4 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sun Feb 28 22:30:51 2010 +0100
+++ b/src/HOL/Tools/Function/function.ML	Sun Feb 28 23:51:31 2010 +0100
@@ -146,7 +146,7 @@
         let
           val totality = Thm.close_derivation totality
           val remove_domain_condition =
-            full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
+            full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])
           val tsimps = map remove_domain_condition psimps
           val tinduct = map remove_domain_condition pinducts