--- a/src/HOL/Tools/recdef.ML Mon Mar 10 17:52:30 2014 +0100
+++ b/src/HOL/Tools/recdef.ML Mon Mar 10 18:06:23 2014 +0100
@@ -164,7 +164,7 @@
val ctxt =
(case opt_src of
NONE => ctxt0
- | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
+ | SOME src => #2 (Args.syntax (Method.sections recdef_modifiers) src ctxt0));
val {simps, congs, wfs} = get_hints ctxt;
val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
in (ctxt', rev (map snd congs), wfs) end;