diff -r 19b47bfac6ef -r 9e7d1c139569 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Thu Apr 18 17:07:01 2013 +0200
@@ -157,11 +157,13 @@
 fun curry_n arity = funpow (arity - 1) mk_curry;
 fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_split;
 
-val curry_uncurry_ss = HOL_basic_ss addsimps
-  [@{thm Product_Type.curry_split}, @{thm Product_Type.split_curry}]
+val curry_uncurry_ss =
+  simpset_of (put_simpset HOL_basic_ss @{context}
+    addsimps [@{thm Product_Type.curry_split}, @{thm Product_Type.split_curry}])
 
-val split_conv_ss = HOL_basic_ss addsimps
-  [@{thm Product_Type.split_conv}];
+val split_conv_ss =
+  simpset_of (put_simpset HOL_basic_ss @{context}
+    addsimps [@{thm Product_Type.split_conv}]);
 
 fun mk_curried_induct args ctxt ccurry cuncurry rule =
   let
@@ -187,12 +189,12 @@
 
     val inst_rule' = inst_rule
       |> Tactic.rule_by_tactic ctxt
-        (Simplifier.simp_tac curry_uncurry_ss 4
-         THEN Simplifier.simp_tac curry_uncurry_ss 3
+        (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 4
+         THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3
          THEN CONVERSION (split_params_conv ctxt
            then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3)
       |> Drule.instantiate' [] [NONE, NONE, SOME P_inst, SOME x_inst]
-      |> Simplifier.full_simplify split_conv_ss
+      |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt)
       |> singleton (Variable.export ctxt' ctxt)
   in
     inst_rule'
@@ -253,7 +255,7 @@
     val unfold =
       (cterm_instantiate' (map (SOME o cert) [uncurry, F, curry]) fixp_eq
         OF [mono_thm, f_def])
-      |> Tactic.rule_by_tactic lthy (Simplifier.simp_tac curry_uncurry_ss 1);
+      |> Tactic.rule_by_tactic lthy (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy) 1);
 
     val mk_raw_induct =
       mk_curried_induct args args_ctxt (cert curry) (cert uncurry)