# HG changeset patch
# User wenzelm
# Date 1243248558 -7200
# Node ID 4c34331a88f9495645747e60a0368af5f16e5afa
# Parent  ed40b987a4748cbb1f6f552bc08f3a1a59d88ec0
simplified method syntax;

diff -r ed40b987a474 -r 4c34331a88f9 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Mon May 25 12:49:05 2009 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Mon May 25 12:49:18 2009 +0200
@@ -170,7 +170,7 @@
     val ctxt =
       (case opt_src of
         NONE => ctxt0
-      | SOME src => Method.only_sectioned_args recdef_modifiers I src ctxt0);
+      | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
     val {simps, congs, wfs} = get_hints ctxt;
     val cs = local_claset_of ctxt;
     val ss = local_simpset_of ctxt addsimps simps;