# HG changeset patch
# User wenzelm
# Date 1326295439 -3600
# Node ID afda84cd4d4b36b5b0d4fae7519222fc31f3c33b
# Parent  e81b5673ae01acb7cbd24e197d7f112a189bc2e2
refer to imp_cong from HOL, not Drule (!) -- cf. 4ed94d92ae19;

diff -r e81b5673ae01 -r afda84cd4d4b src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Wed Jan 11 15:12:57 2012 +0100
+++ b/src/HOL/Tools/recdef.ML	Wed Jan 11 16:23:59 2012 +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 |> Simplifier.del_cong imp_cong);
+      |> Simplifier.map_simpset (fn ss => ss addsimps simps |> Simplifier.del_cong @{thm 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 |> Simplifier.del_cong imp_cong);
+      |> Simplifier.map_simpset (fn ss => ss addsimps simps |> Simplifier.del_cong @{thm imp_cong});
   in (ctxt', rev (map snd congs), wfs) end;