# HG changeset patch
# User wenzelm
# Date 1243688423 -7200
# Node ID 00a9c674cf40935ead45de87f6b9e3f9f57517de
# Parent  4392ad4270944175b7494452e0a3684b28064268
eliminated old Method.add_method(s);

diff -r 4392ad427094 -r 00a9c674cf40 NEWS
--- a/NEWS	Sat May 30 14:26:33 2009 +0200
+++ b/NEWS	Sat May 30 15:00:23 2009 +0200
@@ -26,6 +26,14 @@
 by the code generator; see Predicate.thy for an example.
 
 
+*** ML ***
+
+* Eliminated old Method.add_methods and related cominators for "method
+args".  INCOMPATIBILITY, need to use simplified Method.setup
+introduced in Isabelle2009.
+
+
+
 New in Isabelle2009 (April 2009)
 --------------------------------
 
diff -r 4392ad427094 -r 00a9c674cf40 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat May 30 14:26:33 2009 +0200
+++ b/src/Pure/Isar/method.ML	Sat May 30 15:00:23 2009 +0200
@@ -75,10 +75,6 @@
   val defined: theory -> string -> bool
   val method: theory -> src -> Proof.context -> method
   val method_i: theory -> src -> Proof.context -> method
-  val add_methods: (bstring * (src -> Proof.context -> method) * string) list
-    -> theory -> theory
-  val add_method: bstring * (src -> Proof.context -> method) * string
-    -> theory -> theory
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
   val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
@@ -343,6 +339,10 @@
     |> Pretty.chunks |> Pretty.writeln
   end;
 
+fun add_method name meth comment thy = thy |> Methods.map (fn meths =>
+  #2 (NameSpace.define (Sign.naming_of thy) (name, ((meth, comment), stamp ())) meths)
+    handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup));
+
 
 (* get methods *)
 
@@ -363,27 +363,13 @@
 fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (Methods.get thy)));
 
 
-(* add method *)
-
-fun add_methods raw_meths thy =
-  let
-    val new_meths = raw_meths |> map (fn (name, f, comment) =>
-      (Binding.name name, ((f, comment), stamp ())));
-
-    fun add meths = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_meths meths
-      handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
-  in Methods.map add thy end;
-
-val add_method = add_methods o Library.single;
-
-
 (* method setup *)
 
 fun syntax scan = Args.context_syntax "method" scan;
 
-fun setup name scan comment =
-  add_methods [(Binding.name_of name,
-    fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end, comment)];
+fun setup name scan =
+  add_method name
+    (fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end);
 
 fun method_setup name (txt, pos) cmt =
   Context.theory_map (ML_Context.expression pos