1.1 --- a/src/Pure/Isar/method.ML	Sat Oct 24 19:04:57 2009 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sat Oct 24 19:20:03 2009 +0200
     1.3 @@ -322,27 +322,25 @@
     1.4  
     1.5  structure Methods = TheoryDataFun
     1.6  (
     1.7 -  type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
     1.8 +  type T = ((src -> Proof.context -> method) * string) NameSpace.table;
     1.9    val empty = NameSpace.empty_table;
    1.10    val copy = I;
    1.11    val extend = I;
    1.12 -  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
    1.13 -    error ("Attempt to merge different versions of method " ^ quote dup);
    1.14 +  fun merge _ tables : T = NameSpace.merge_tables tables;
    1.15  );
    1.16  
    1.17  fun print_methods thy =
    1.18    let
    1.19      val meths = Methods.get thy;
    1.20 -    fun prt_meth (name, ((_, comment), _)) = Pretty.block
    1.21 +    fun prt_meth (name, (_, comment)) = Pretty.block
    1.22        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.23    in
    1.24      [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
    1.25      |> Pretty.chunks |> Pretty.writeln
    1.26    end;
    1.27  
    1.28 -fun add_method name meth comment thy = thy |> Methods.map (fn meths =>
    1.29 -  #2 (NameSpace.define (Sign.naming_of thy) (name, ((meth, comment), stamp ())) meths)
    1.30 -    handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup));
    1.31 +fun add_method name meth comment thy = thy
    1.32 +  |> Methods.map (#2 o NameSpace.define true (Sign.naming_of thy) (name, (meth, comment)));
    1.33  
    1.34  
    1.35  (* get methods *)
    1.36 @@ -357,7 +355,7 @@
    1.37        let val ((name, _), pos) = Args.dest_src src in
    1.38          (case Symtab.lookup meths name of
    1.39            NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
    1.40 -        | SOME ((mth, _), _) => (Position.report (Markup.method name) pos; mth src))
    1.41 +        | SOME (mth, _) => (Position.report (Markup.method name) pos; mth src))
    1.42        end;
    1.43    in meth end;
    1.44