--- a/src/Pure/Isar/method.ML Fri Dec 05 11:42:27 2008 +0100
+++ b/src/Pure/Isar/method.ML Fri Dec 05 18:42:37 2008 +0100
@@ -448,9 +448,9 @@
fun add_methods raw_meths thy =
let
val new_meths = raw_meths |> map (fn (name, f, comment) =>
- (name, ((f, comment), stamp ())));
+ (Binding.name name, ((f, comment), stamp ())));
- fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
+ fun add meths = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_meths meths
handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
in Methods.map add thy end;