diff -r 07155da3b2f4 -r 66fcc9882784 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Tools/recdef.ML	Fri May 13 23:58:40 2011 +0200
@@ -167,7 +167,7 @@
       | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
     val {simps, congs, wfs} = get_hints ctxt;
     val ctxt' = ctxt
-      |> Context.proof_map (Simplifier.map_ss (fn ss => ss addsimps simps delcongs [imp_cong]));
+      |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
   in (ctxt', rev (map snd congs), wfs) end;
 
 fun prepare_hints_i thy () =
@@ -175,7 +175,7 @@
     val ctxt = Proof_Context.init_global thy;
     val {simps, congs, wfs} = get_global_hints thy;
     val ctxt' = ctxt
-      |> Context.proof_map (Simplifier.map_ss (fn ss => ss addsimps simps delcongs [imp_cong]));
+      |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
   in (ctxt', rev (map snd congs), wfs) end;