changeset 45228 | aa3ad19c05d5 |
parent 42813 | 6c841fa92fa2 |
child 45375 | 7fe19930dfc9 |
--- 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 *)