author | wenzelm |
Mon, 25 May 2009 12:49:18 +0200 | |
changeset 31243 | 4c34331a88f9 |
parent 31242 | ed40b987a474 |
child 31244 | 4ed31c673baf |
--- 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;