# HG changeset patch
# User wenzelm
# Date 1153303921 -7200
# Node ID b71f4f4c6b1ec33e66a3f91d2614f550508c9315
# Parent  28638d2a6bc7ea7cb7a6162c0cee43f48d36648f
export make_context, is_declared;

diff -r 28638d2a6bc7 -r b71f4f4c6b1e src/Pure/name.ML
--- a/src/Pure/name.ML	Wed Jul 19 12:12:00 2006 +0200
+++ b/src/Pure/name.ML	Wed Jul 19 12:12:01 2006 +0200
@@ -17,7 +17,9 @@
   val clean: string -> string
   type context
   val context: context
+  val make_context: string list -> context
   val declare: string -> context -> context
+  val is_declared: context -> string -> bool
   val invents: context -> string -> int -> string list
   val invent_list: string list -> string -> int -> string list
   val variants: string list -> context -> string list * context
@@ -77,6 +79,7 @@
 fun declare_renaming (x, x') (Context tab) =
   Context (Symtab.update (clean x, SOME (clean x')) tab);
 
+fun is_declared (Context tab) = Symtab.defined tab;
 fun declared (Context tab) = Symtab.lookup tab;
 
 val context = Context Symtab.empty |> fold declare ["", "'"];
@@ -90,7 +93,7 @@
     fun invs _ 0 = []
       | invs x n =
           let val x' = Symbol.bump_string x in
-            if is_some (declared ctxt x) then invs x' n
+            if is_declared ctxt x then invs x' n
             else x :: invs x' (n - 1)
           end;
   in invs o clean end;
@@ -111,7 +114,7 @@
 
     val (x, n) = clean_index (name, 0);
     val (x', ctxt') =
-      if is_none (declared ctxt x) then (x, declare x ctxt)
+      if not (is_declared ctxt x) then (x, declare x ctxt)
       else
         let
           val x0 = Symbol.bump_init x;