--- a/src/HOL/Tools/recdef.ML Wed Nov 23 22:07:55 2011 +0100
+++ b/src/HOL/Tools/recdef.ML Wed Nov 23 22:59:39 2011 +0100
@@ -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
- |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
+ |> Simplifier.map_simpset (fn ss => ss addsimps simps |> Simplifier.del_cong 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
- |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
+ |> Simplifier.map_simpset (fn ss => ss addsimps simps |> Simplifier.del_cong imp_cong);
in (ctxt', rev (map snd congs), wfs) end;