src/Pure/name.ML
changeset 20158 b71f4f4c6b1e
parent 20121 848fc1a1d355
child 20174 c057b3618963
     1.1 --- a/src/Pure/name.ML	Wed Jul 19 12:12:00 2006 +0200
     1.2 +++ b/src/Pure/name.ML	Wed Jul 19 12:12:01 2006 +0200
     1.3 @@ -17,7 +17,9 @@
     1.4    val clean: string -> string
     1.5    type context
     1.6    val context: context
     1.7 +  val make_context: string list -> context
     1.8    val declare: string -> context -> context
     1.9 +  val is_declared: context -> string -> bool
    1.10    val invents: context -> string -> int -> string list
    1.11    val invent_list: string list -> string -> int -> string list
    1.12    val variants: string list -> context -> string list * context
    1.13 @@ -77,6 +79,7 @@
    1.14  fun declare_renaming (x, x') (Context tab) =
    1.15    Context (Symtab.update (clean x, SOME (clean x')) tab);
    1.16  
    1.17 +fun is_declared (Context tab) = Symtab.defined tab;
    1.18  fun declared (Context tab) = Symtab.lookup tab;
    1.19  
    1.20  val context = Context Symtab.empty |> fold declare ["", "'"];
    1.21 @@ -90,7 +93,7 @@
    1.22      fun invs _ 0 = []
    1.23        | invs x n =
    1.24            let val x' = Symbol.bump_string x in
    1.25 -            if is_some (declared ctxt x) then invs x' n
    1.26 +            if is_declared ctxt x then invs x' n
    1.27              else x :: invs x' (n - 1)
    1.28            end;
    1.29    in invs o clean end;
    1.30 @@ -111,7 +114,7 @@
    1.31  
    1.32      val (x, n) = clean_index (name, 0);
    1.33      val (x', ctxt') =
    1.34 -      if is_none (declared ctxt x) then (x, declare x ctxt)
    1.35 +      if not (is_declared ctxt x) then (x, declare x ctxt)
    1.36        else
    1.37          let
    1.38            val x0 = Symbol.bump_init x;