# HG changeset patch
# User wenzelm
# Date 1303570932 -7200
# Node ID bbce02fcba60866c5a6598eea0d046a2c7c68a4b
# Parent  1ba52683512a414a99219d3ffe3e4c2f339d98c3
added Name_Space.check/get convenience;

diff -r 1ba52683512a -r bbce02fcba60 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sat Apr 23 16:30:00 2011 +0200
+++ b/src/Pure/General/name_space.ML	Sat Apr 23 17:02:12 2011 +0200
@@ -49,6 +49,8 @@
   val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
   val alias: naming -> binding -> string -> T -> T
   type 'a table = T * 'a Symtab.table
+  val check: Proof.context -> 'a table -> xstring * Position.T -> string
+  val get: 'a table -> string -> 'a
   val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
   val empty_table: string -> 'a table
   val merge_tables: 'a table * 'a table -> 'a table
@@ -93,6 +95,8 @@
   error ("Duplicate " ^ kind ^ " declaration " ^
     print_entry true kind entry1 ^ " vs. " ^ print_entry true kind entry2);
 
+fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name;
+
 
 (* datatype T *)
 
@@ -367,8 +371,7 @@
       |> fold (add_name name) accs
       |> map_name_space (fn (kind, internals, entries) =>
         let
-          val _ = Symtab.defined entries name orelse
-            error ("Undefined " ^ kind ^ " " ^ quote name);
+          val _ = Symtab.defined entries name orelse error (undefined kind name);
           val entries' = entries
             |> Symtab.map_entry name (fn (externals, entry) =>
               (Library.merge (op =) (externals, accs'), entry))
@@ -381,6 +384,18 @@
 
 type 'a table = T * 'a Symtab.table;
 
+fun check ctxt (space, tab) (xname, pos) =
+  let val name = intern space xname in
+    if Symtab.defined tab name
+    then (Context_Position.report ctxt pos (markup space name); name)
+    else error (undefined (kind_of space) name ^ Position.str_of pos)
+  end;
+
+fun get (space, tab) name =
+  (case Symtab.lookup tab name of
+    SOME x => x
+  | NONE => error (undefined (kind_of space) name));
+
 fun define ctxt strict naming (binding, x) (space, tab) =
   let val (name, space') = declare ctxt strict naming binding space
   in (name, (space', Symtab.update (name, x) tab)) end;
diff -r 1ba52683512a -r bbce02fcba60 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Apr 23 16:30:00 2011 +0200
+++ b/src/Pure/simplifier.ML	Sat Apr 23 17:02:12 2011 +0200
@@ -158,22 +158,8 @@
 
 (* get simprocs *)
 
-fun undef_simproc name = "Undefined simplification procedure: " ^ quote name;
-
-fun check_simproc ctxt (xname, pos) =
-  let
-    val (space, tab) = get_simprocs ctxt;
-    val name = Name_Space.intern space xname;
-  in
-    if Symtab.defined tab name then
-      (Context_Position.report ctxt pos (Name_Space.markup space name); name)
-    else error (undef_simproc name ^ Position.str_of pos)
-  end;
-
-fun the_simproc ctxt name =
-  (case Symtab.lookup (#2 (get_simprocs ctxt)) name of
-    SOME proc => proc
-  | NONE => error (undef_simproc name));
+fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt);
+val the_simproc = Name_Space.get o get_simprocs;
 
 val _ =
   ML_Antiquote.value "simproc"