diff -r 010eefa0a4f3 -r 7a86358a3c0b src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Fri Dec 13 23:53:02 2013 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Sat Dec 14 17:28:05 2013 +0100
@@ -180,6 +180,7 @@
     val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
     val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
   in 
+    (* FIXME ctxt vs. ctxt' (!?) *)
     rule
     |> cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry), NONE, SOME (cert P_inst)]
     |> Tactic.rule_by_tactic ctxt
@@ -188,7 +189,7 @@
        THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
     |> (fn thm => thm OF [mono_thm, f_def])
     |> Conv.fconv_rule (Conv.concl_conv ~1    (* simplify conclusion *)
-         (Raw_Simplifier.rewrite false [mk_meta_eq @{thm Product_Type.curry_split}])) 
+         (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_split}]))
     |> singleton (Variable.export ctxt' ctxt)
   end