# HG changeset patch
# User wenzelm
# Date 1210789829 -7200
# Node ID 9454a8bd1114d8dd1059c893d979c528a383020f
# Parent  bfa1944e523891f7910ef8ea04e3232458c48147
added intern, defined;

diff -r bfa1944e5238 -r 9454a8bd1114 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed May 14 20:30:05 2008 +0200
+++ b/src/Pure/Isar/method.ML	Wed May 14 20:30:29 2008 +0200
@@ -70,6 +70,8 @@
   val done_text: text
   val sorry_text: bool -> text
   val finish_text: text option * bool -> Position.T -> text
+  val intern: theory -> xstring -> string
+  val defined: theory -> string -> bool
   val method: theory -> src -> Proof.context -> method
   val method_i: theory -> src -> Proof.context -> method
   val add_methods: (bstring * (src -> Proof.context -> method) * string) list
@@ -424,6 +426,9 @@
 
 (* get methods *)
 
+val intern = NameSpace.intern o #1 o Methods.get;
+val defined = Symtab.defined o #2 o Methods.get;
+
 fun method_i thy =
   let
     val meths = #2 (Methods.get thy);