Inttab.defined;
authorwenzelm
Tue Jul 19 20:47:01 2005 +0200 (2005-07-19)
changeset 1689440f80823b451
parent 16893 0cc94e6f6ae5
child 16895 df67fc190e06
Inttab.defined;
src/Pure/General/graph.ML
src/Pure/General/table.ML
src/Pure/Isar/isar_output.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof_context.ML
src/Pure/Thy/thm_deps.ML
src/Pure/context.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/General/graph.ML	Tue Jul 19 20:47:00 2005 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Tue Jul 19 20:47:01 2005 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  val empty_keys = Table.empty: keys;
     1.5  
     1.6  infix mem_keys;
     1.7 -fun x mem_keys tab = is_some (Table.lookup (tab: keys, x));
     1.8 +fun x mem_keys tab = Table.defined (tab: keys) x;
     1.9  
    1.10  infix ins_keys;
    1.11  fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys);
     2.1 --- a/src/Pure/General/table.ML	Tue Jul 19 20:47:00 2005 +0200
     2.2 +++ b/src/Pure/General/table.ML	Tue Jul 19 20:47:01 2005 +0200
     2.3 @@ -211,7 +211,7 @@
     2.4  fun extend (table, args) =
     2.5    let
     2.6      fun add (key, x) (tab, dups) =
     2.7 -      if is_some (lookup (tab, key)) then (tab, key :: dups)
     2.8 +      if defined tab key then (tab, key :: dups)
     2.9        else (update ((key, x), tab), dups);
    2.10    in
    2.11      (case fold add args (table, []) of
     3.1 --- a/src/Pure/Isar/isar_output.ML	Tue Jul 19 20:47:00 2005 +0200
     3.2 +++ b/src/Pure/Isar/isar_output.ML	Tue Jul 19 20:47:01 2005 +0200
     3.3 @@ -60,7 +60,7 @@
     3.4  
     3.5  
     3.6  fun add_item kind (tab, (name, x)) =
     3.7 - (if is_none (Symtab.lookup (tab, name)) then ()
     3.8 + (if not (Symtab.defined tab name) then ()
     3.9    else warning ("Redefined antiquotation output " ^ kind ^ ": " ^ quote name);
    3.10    Symtab.update ((name, x), tab));
    3.11  
     4.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 19 20:47:00 2005 +0200
     4.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 19 20:47:01 2005 +0200
     4.3 @@ -198,7 +198,7 @@
     4.4    (Scan.extend_lexicon lex (map Symbol.explode keywords))));
     4.5  
     4.6  fun add_parser (tab, Parser (name, (comment, kind, markup), int_only, parse)) =
     4.7 - (if is_none (Symtab.lookup (tab, name)) then ()
     4.8 + (if not (Symtab.defined tab name) then ()
     4.9    else warning ("Redefined outer syntax command " ^ quote name);
    4.10    Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));
    4.11  
     5.1 --- a/src/Pure/Isar/proof_context.ML	Tue Jul 19 20:47:00 2005 +0200
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Jul 19 20:47:01 2005 +0200
     5.3 @@ -224,8 +224,7 @@
     5.4  val type_occs_of = #4 o defaults_of;
     5.5  
     5.6  fun is_fixed ctxt x = exists (equal x o #2) (fixes_of ctxt);
     5.7 -fun is_known ctxt x =
     5.8 -  is_some (Vartab.lookup (#1 (defaults_of ctxt), (x, ~1))) orelse is_fixed ctxt x;
     5.9 +fun is_known ctxt x = Vartab.defined (#1 (defaults_of ctxt)) (x, ~1) orelse is_fixed ctxt x;
    5.10  
    5.11  
    5.12  
    5.13 @@ -659,7 +658,7 @@
    5.14      val occs_inner = type_occs_of inner;
    5.15      val occs_outer = type_occs_of outer;
    5.16      fun add a gen =
    5.17 -      if is_some (Symtab.lookup (occs_outer, a)) orelse
    5.18 +      if Symtab.defined occs_outer a orelse
    5.19          exists still_fixed (Symtab.lookup_multi (occs_inner, a))
    5.20        then gen else a :: gen;
    5.21    in fn tfrees => fold add tfrees [] end;
     6.1 --- a/src/Pure/Thy/thm_deps.ML	Tue Jul 19 20:47:00 2005 +0200
     6.2 +++ b/src/Pure/Thy/thm_deps.ML	Tue Jul 19 20:47:01 2005 +0200
     6.3 @@ -39,7 +39,7 @@
     6.4        let val ((name, tags), prf') = dest_thm_axm prf
     6.5        in
     6.6          if name <> "" andalso not (Drule.has_internal tags) then
     6.7 -          if is_none (Symtab.lookup (gra, name)) then
     6.8 +          if not (Symtab.defined gra name) then
     6.9              let
    6.10                val (gra', parents') = make_deps_graph ((gra, []), prf');
    6.11                val prefx = #1 (Library.split_last (NameSpace.unpack name));
     7.1 --- a/src/Pure/context.ML	Tue Jul 19 20:47:00 2005 +0200
     7.2 +++ b/src/Pure/context.ML	Tue Jul 19 20:47:01 2005 +0200
     7.3 @@ -251,7 +251,7 @@
     7.4    else thy;
     7.5  
     7.6  fun check_ins id ids =
     7.7 -  if draft_id id orelse is_some (Inttab.lookup (ids, #1 id)) then ids
     7.8 +  if draft_id id orelse Inttab.defined ids (#1 id) then ids
     7.9    else if Inttab.exists (equal (#2 id) o #2) ids then
    7.10      raise TERM ("Different versions of theory component " ^ quote (#2 id), [])
    7.11    else Inttab.update (id, ids);
    7.12 @@ -274,7 +274,7 @@
    7.13  
    7.14  fun proper_subthy
    7.15      (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =
    7.16 -  is_some (Inttab.lookup (ids, i)) orelse is_some (Inttab.lookup (iids, i));
    7.17 +  Inttab.defined ids i orelse Inttab.defined iids i;
    7.18  
    7.19  fun subthy thys = eq_thy thys orelse proper_subthy thys;
    7.20  
     8.1 --- a/src/Pure/sign.ML	Tue Jul 19 20:47:00 2005 +0200
     8.2 +++ b/src/Pure/sign.ML	Tue Jul 19 20:47:01 2005 +0200
     8.3 @@ -260,9 +260,7 @@
     8.4    (case const_type thy c of SOME T => T
     8.5    | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
     8.6  
     8.7 -fun declared_tyname thy c =
     8.8 -  is_some (Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy))), c));
     8.9 -
    8.10 +val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
    8.11  val declared_const = is_some oo const_type;
    8.12  
    8.13