src/Pure/Isar/method.ML

     val src' = map Token.init_assignable src;
     val ctxt' = Context_Position.not_really ctxt;
     val _ = Seq.pull (method ctxt' src' ctxt' [] (ctxt', Goal.protect 0 Drule.dummy_thm));
   in map Token.closure src' end;
 
-val closure = Config.bool (Config.declare ("Method.closure", \<^here>) (K (Config.Bool true)));
+val closure = Config.declare_bool ("Method.closure", \<^here>) (K true);
 
 fun method_cmd ctxt =
   check_src ctxt #>
   Config.get ctxt closure ? method_closure ctxt #>
   method ctxt;

 fun modifier attribute pos : modifier = {init = I, attribute = attribute, pos = pos};
 
 
 (* sections *)
 
-val old_section_parser =
-  Config.bool (Config.declare ("Method.old_section_parser", \<^here>) (K (Config.Bool false)));
+val old_section_parser = Config.declare_bool ("Method.old_section_parser", \<^here>) (K false);
 
 local
 
 fun thms ss =
   Scan.repeats (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm);