author | wenzelm |
Fri, 21 Oct 2011 11:26:14 +0200 | |
changeset 45228 | aa3ad19c05d5 |
parent 45227 | f00a1aee5bc2 |
child 45229 | 84f0b18a6e6e |
--- 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 *)