# HG changeset patch
# User wenzelm
# Date 1121798821 -7200
# Node ID 40f80823b45153bec92f0c0205a16156c939d252
# Parent  0cc94e6f6ae5bbf23baec861b9aa6da140e16d43
Inttab.defined;

diff -r 0cc94e6f6ae5 -r 40f80823b451 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Tue Jul 19 20:47:00 2005 +0200
+++ b/src/Pure/General/graph.ML	Tue Jul 19 20:47:01 2005 +0200
@@ -63,7 +63,7 @@
 val empty_keys = Table.empty: keys;
 
 infix mem_keys;
-fun x mem_keys tab = is_some (Table.lookup (tab: keys, x));
+fun x mem_keys tab = Table.defined (tab: keys) x;
 
 infix ins_keys;
 fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys);
diff -r 0cc94e6f6ae5 -r 40f80823b451 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Tue Jul 19 20:47:00 2005 +0200
+++ b/src/Pure/General/table.ML	Tue Jul 19 20:47:01 2005 +0200
@@ -211,7 +211,7 @@
 fun extend (table, args) =
   let
     fun add (key, x) (tab, dups) =
-      if is_some (lookup (tab, key)) then (tab, key :: dups)
+      if defined tab key then (tab, key :: dups)
       else (update ((key, x), tab), dups);
   in
     (case fold add args (table, []) of
diff -r 0cc94e6f6ae5 -r 40f80823b451 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Tue Jul 19 20:47:00 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML	Tue Jul 19 20:47:01 2005 +0200
@@ -60,7 +60,7 @@
 
 
 fun add_item kind (tab, (name, x)) =
- (if is_none (Symtab.lookup (tab, name)) then ()
+ (if not (Symtab.defined tab name) then ()
   else warning ("Redefined antiquotation output " ^ kind ^ ": " ^ quote name);
   Symtab.update ((name, x), tab));
 
diff -r 0cc94e6f6ae5 -r 40f80823b451 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 19 20:47:00 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 19 20:47:01 2005 +0200
@@ -198,7 +198,7 @@
   (Scan.extend_lexicon lex (map Symbol.explode keywords))));
 
 fun add_parser (tab, Parser (name, (comment, kind, markup), int_only, parse)) =
- (if is_none (Symtab.lookup (tab, name)) then ()
+ (if not (Symtab.defined tab name) then ()
   else warning ("Redefined outer syntax command " ^ quote name);
   Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));
 
diff -r 0cc94e6f6ae5 -r 40f80823b451 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jul 19 20:47:00 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 19 20:47:01 2005 +0200
@@ -224,8 +224,7 @@
 val type_occs_of = #4 o defaults_of;
 
 fun is_fixed ctxt x = exists (equal x o #2) (fixes_of ctxt);
-fun is_known ctxt x =
-  is_some (Vartab.lookup (#1 (defaults_of ctxt), (x, ~1))) orelse is_fixed ctxt x;
+fun is_known ctxt x = Vartab.defined (#1 (defaults_of ctxt)) (x, ~1) orelse is_fixed ctxt x;
 
 
 
@@ -659,7 +658,7 @@
     val occs_inner = type_occs_of inner;
     val occs_outer = type_occs_of outer;
     fun add a gen =
-      if is_some (Symtab.lookup (occs_outer, a)) orelse
+      if Symtab.defined occs_outer a orelse
         exists still_fixed (Symtab.lookup_multi (occs_inner, a))
       then gen else a :: gen;
   in fn tfrees => fold add tfrees [] end;
diff -r 0cc94e6f6ae5 -r 40f80823b451 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Tue Jul 19 20:47:00 2005 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Tue Jul 19 20:47:01 2005 +0200
@@ -39,7 +39,7 @@
       let val ((name, tags), prf') = dest_thm_axm prf
       in
         if name <> "" andalso not (Drule.has_internal tags) then
-          if is_none (Symtab.lookup (gra, name)) then
+          if not (Symtab.defined gra name) then
             let
               val (gra', parents') = make_deps_graph ((gra, []), prf');
               val prefx = #1 (Library.split_last (NameSpace.unpack name));
diff -r 0cc94e6f6ae5 -r 40f80823b451 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Jul 19 20:47:00 2005 +0200
+++ b/src/Pure/context.ML	Tue Jul 19 20:47:01 2005 +0200
@@ -251,7 +251,7 @@
   else thy;
 
 fun check_ins id ids =
-  if draft_id id orelse is_some (Inttab.lookup (ids, #1 id)) then ids
+  if draft_id id orelse Inttab.defined ids (#1 id) then ids
   else if Inttab.exists (equal (#2 id) o #2) ids then
     raise TERM ("Different versions of theory component " ^ quote (#2 id), [])
   else Inttab.update (id, ids);
@@ -274,7 +274,7 @@
 
 fun proper_subthy
     (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =
-  is_some (Inttab.lookup (ids, i)) orelse is_some (Inttab.lookup (iids, i));
+  Inttab.defined ids i orelse Inttab.defined iids i;
 
 fun subthy thys = eq_thy thys orelse proper_subthy thys;
 
diff -r 0cc94e6f6ae5 -r 40f80823b451 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Jul 19 20:47:00 2005 +0200
+++ b/src/Pure/sign.ML	Tue Jul 19 20:47:01 2005 +0200
@@ -260,9 +260,7 @@
   (case const_type thy c of SOME T => T
   | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
 
-fun declared_tyname thy c =
-  is_some (Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy))), c));
-
+val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
 val declared_const = is_some oo const_type;