diff -r f00a1aee5bc2 -r aa3ad19c05d5 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Fri Oct 21 10:37:03 2011 +0200 +++ b/src/Pure/Isar/method.ML Fri Oct 21 11:26:14 2011 +0200 @@ -366,7 +366,7 @@ end; in meth end; -fun method thy = method_i thy o Args.map_name (Name_Space.intern (#1 (Methods.get thy))); +fun method thy = method_i thy o Args.map_name (intern thy); (* method setup *)