--- a/src/HOL/Tools/Function/function.ML Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Tools/Function/function.ML Thu Apr 18 17:07:01 2013 +0200
@@ -187,7 +187,8 @@
let
val totality = Thm.close_derivation totality
val remove_domain_condition =
- full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])
+ full_simplify (put_simpset HOL_basic_ss lthy
+ addsimps [totality, @{thm True_implies_equals}])
val tsimps = map remove_domain_condition psimps
val tinduct = map remove_domain_condition pinducts