--- a/src/HOL/Tools/recdef.ML Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Tools/recdef.ML Thu Apr 18 17:07:01 2013 +0200
@@ -166,16 +166,14 @@
NONE => ctxt0
| 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 |> Simplifier.del_cong @{thm imp_cong});
+ val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
in (ctxt', rev (map snd congs), wfs) end;
fun prepare_hints_i thy () =
let
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 |> Simplifier.del_cong @{thm imp_cong});
+ val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
in (ctxt', rev (map snd congs), wfs) end;