src/Pure/Isar/method.ML
changeset 56025 d74fed45fa8b
parent 55997 9dc5ce83202c
child 56026 893fe12639bc
--- a/src/Pure/Isar/method.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/Isar/method.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -351,12 +351,12 @@
 (* get methods *)
 
 fun method ctxt =
-  let val (_, tab) = get_methods ctxt in
+  let val table = get_methods ctxt in
     fn src =>
       let val ((name, _), pos) = Args.dest_src src in
-        (case Symtab.lookup tab name of
+        (case Name_Space.lookup_key table name of
           NONE => error ("Undefined method: " ^ quote name ^ Position.here pos)
-        | SOME (meth, _) => meth src)
+        | SOME (_, (meth, _)) => meth src)
       end
   end;