# HG changeset patch # User wenzelm # Date 1125593330 -7200 # Node ID 6cd180204582911ce4dc76c1ada18a4d575a8fa4 # Parent b41d8e290bf899ed383ace24b572492543b97ae8 curried_lookup/update; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/General/graph.ML --- a/src/Pure/General/graph.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/General/graph.ML Thu Sep 01 18:48:50 2005 +0200 @@ -86,11 +86,11 @@ fun maximals (Graph tab) = Table.fold (fn (m, (_, (_, []))) => cons m | _ => I) tab []; fun get_entry (Graph tab) x = - (case Table.lookup (tab, x) of + (case Table.curried_lookup tab x of SOME entry => entry | NONE => raise UNDEF x); -fun map_entry x f (G as Graph tab) = Graph (Table.update ((x, f (get_entry G x)), tab)); +fun map_entry x f (G as Graph tab) = Graph (Table.curried_update (x, f (get_entry G x)) tab); (* nodes *) @@ -142,7 +142,7 @@ (* nodes *) fun new_node (x, info) (Graph tab) = - Graph (Table.update_new ((x, (info, ([], []))), tab)); + Graph (Table.curried_update_new (x, (info, ([], []))) tab); fun default_node (x, info) (Graph tab) = Graph (Table.default (x, (info, ([], []))) tab); diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/General/name_space.ML Thu Sep 01 18:48:50 2005 +0200 @@ -113,7 +113,7 @@ val empty = NameSpace Symtab.empty; fun lookup (NameSpace tab) xname = - (case Symtab.lookup (tab, xname) of + (case Symtab.curried_lookup tab xname of NONE => (xname, true) | SOME ([], []) => (xname, true) | SOME ([name], _) => (name, true) @@ -150,7 +150,7 @@ (* basic operations *) fun map_space f xname (NameSpace tab) = - NameSpace (Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab)); + NameSpace (Symtab.curried_update (xname, f (if_none (Symtab.curried_lookup tab xname) ([], []))) tab); fun del (name: string) = remove (op =) name; fun add name names = name :: del name names; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/General/output.ML Thu Sep 01 18:48:50 2005 +0200 @@ -84,7 +84,7 @@ exception MISSING_DEFAULT_OUTPUT; -fun lookup_mode name = Symtab.lookup (! modes, name); +fun lookup_mode name = Symtab.curried_lookup (! modes) name; fun get_mode () = (case Library.get_first lookup_mode (! print_mode) of SOME p => p @@ -141,7 +141,7 @@ fun add_mode name (f, g, h) = (if is_none (lookup_mode name) then () else warning ("Redeclaration of symbol print mode: " ^ quote name); - modes := Symtab.update ((name, {output_width = f, indent = g, raw = h}), ! modes)); + modes := Symtab.curried_update (name, {output_width = f, indent = g, raw = h}) (! modes)); (* produce errors *) diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/General/symbol.ML Thu Sep 01 18:48:50 2005 +0200 @@ -350,7 +350,7 @@ else if is_ascii_quasi s then Quasi else if is_ascii_blank s then Blank else if is_char s then Other - else if_none (Symtab.lookup (symbol_kinds, s)) Other; + else if_none (Symtab.curried_lookup symbol_kinds s) Other; end; fun is_letter s = kind s = Letter; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Isar/attrib.ML Thu Sep 01 18:48:50 2005 +0200 @@ -104,7 +104,7 @@ val attrs = #2 (AttributesData.get thy); fun attr src = let val ((name, _), pos) = Args.dest_src src in - (case Symtab.lookup (attrs, name) of + (case Symtab.curried_lookup attrs name of NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos) | SOME ((p, _), _) => transform_failure (curry ATTRIB_FAIL (name, pos)) (which p src)) end; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Isar/isar_output.ML --- a/src/Pure/Isar/isar_output.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Isar/isar_output.ML Thu Sep 01 18:48:50 2005 +0200 @@ -59,7 +59,7 @@ fun add_item kind (name, x) tab = (if not (Symtab.defined tab name) then () else warning ("Redefined antiquotation " ^ kind ^ ": " ^ quote name); - Symtab.update ((name, x), tab)); + Symtab.curried_update (name, x) tab); in @@ -68,13 +68,13 @@ fun command src = let val ((name, _), pos) = Args.dest_src src in - (case Symtab.lookup (! global_commands, name) of + (case Symtab.curried_lookup (! global_commands) name of NONE => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos) | SOME f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src)) end; fun option (name, s) f () = - (case Symtab.lookup (! global_options, name) of + (case Symtab.curried_lookup (! global_options) name of NONE => error ("Unknown antiquotation option: " ^ quote name) | SOME opt => opt s f ()); diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Isar/locale.ML Thu Sep 01 18:48:50 2005 +0200 @@ -168,7 +168,7 @@ fun tinst_tab_type tinst T = if Symtab.is_empty tinst then T else Term.map_type_tfree - (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T; + (fn (v as (x, _)) => getOpt (Symtab.curried_lookup tinst x, (TFree v))) T; fun tinst_tab_term tinst t = if Symtab.is_empty tinst then t @@ -201,7 +201,7 @@ else (* instantiate terms and types simultaneously *) let fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T) - | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of + | instf (Free (x, T)) = (case Symtab.curried_lookup inst x of NONE => Free (x, tinst_tab_type tinst T) | SOME t => t) | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T) @@ -322,7 +322,7 @@ val sups = List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs); val sups' = map (apfst untermify) sups - in (Termtab.update ((t, (attn, [])), regs), sups') end + in (Termtab.curried_update (t, (attn, [])) regs, sups') end | _ => (regs, [])) end; @@ -331,9 +331,9 @@ fun add_witness ts thm regs = let val t = termify ts; - val (x, thms) = valOf (Termtab.lookup (regs, t)); + val (x, thms) = valOf (Termtab.curried_lookup regs t); in - Termtab.update ((t, (x, thm::thms)), regs) + Termtab.curried_update (t, (x, thm::thms)) regs end; end; @@ -398,9 +398,9 @@ fun put_locale name loc = GlobalLocalesData.map (fn (space, locs, regs) => - (space, Symtab.update ((name, loc), locs), regs)); + (space, Symtab.curried_update (name, loc) locs, regs)); -fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name); +fun get_locale thy name = Symtab.curried_lookup (#2 (GlobalLocalesData.get thy)) name; fun the_locale thy name = (case get_locale thy name of @@ -417,7 +417,7 @@ (* retrieve registration from theory or context *) fun gen_get_registrations get thy_ctxt name = - case Symtab.lookup (get thy_ctxt, name) of + case Symtab.curried_lookup (get thy_ctxt) name of NONE => [] | SOME reg => Registrations.dest reg; @@ -427,7 +427,7 @@ gen_get_registrations LocalLocalesData.get; fun gen_get_registration get thy_of thy_ctxt (name, ps) = - case Symtab.lookup (get thy_ctxt, name) of + case Symtab.curried_lookup (get thy_ctxt) name of NONE => NONE | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps); @@ -452,7 +452,7 @@ map_data (fn regs => let val thy = thy_of thy_ctxt; - val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty); + val reg = getOpt (Symtab.curried_lookup regs name, Registrations.empty); val (reg', sups) = Registrations.insert thy (ps, attn) reg; val _ = if not (null sups) then warning ("Subsumed interpretation(s) of locale " ^ @@ -460,7 +460,7 @@ "\nby interpretation(s) with the following prefix(es):\n" ^ commas_quote (map (fn (_, ((s, _), _)) => s) sups)) else (); - in Symtab.update ((name, reg'), regs) end) thy_ctxt; + in Symtab.curried_update (name, reg') regs end) thy_ctxt; val put_global_registration = gen_put_registration (fn f => @@ -480,13 +480,8 @@ (* add witness theorem to registration in theory or context, ignored if registration not present *) -fun gen_add_witness map (name, ps) thm = - map (fn regs => - let - val reg = valOf (Symtab.lookup (regs, name)); - in - Symtab.update ((name, Registrations.add_witness ps thm reg), regs) - end handle Option => regs); +fun gen_add_witness map_regs (name, ps) thm = + map_regs (Symtab.map_entry name (Registrations.add_witness ps thm)); val add_global_witness = gen_add_witness (fn f => @@ -550,7 +545,7 @@ val loc_int = intern thy loc; val regs = get_regs thy_ctxt; - val loc_regs = Symtab.lookup (regs, loc_int); + val loc_regs = Symtab.curried_lookup regs loc_int; in (case loc_regs of NONE => Pretty.str ("No interpretations in " ^ msg ^ ".") @@ -762,7 +757,7 @@ fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss)); fun params_syn_of syn elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |> - map (apfst (fn x => (x, valOf (Symtab.lookup (syn, x))))); + map (apfst (fn x => (x, valOf (Symtab.curried_lookup syn x)))); (* CB: param_types has the following type: @@ -1008,7 +1003,7 @@ val {params = (ps, qs), elems, ...} = the_locale thy name; val ps' = map (apsnd SOME o #1) ps; val ren = map #1 ps' ~~ - map (fn x => (x, valOf (Symtab.lookup (syn, x)))) xs; + map (fn x => (x, valOf (Symtab.curried_lookup syn x))) xs; val (params', elems') = if null ren then ((ps', qs), map #1 elems) else ((map (apfst (rename ren)) ps', map (rename ren) qs), @@ -1740,7 +1735,7 @@ |> Symtab.make; (* replace parameter names in ids by instantiations *) val vinst = Symtab.make (parms ~~ vts); - fun vinst_names ps = map (fn p => Symtab.lookup (vinst, p) |> valOf) ps; + fun vinst_names ps = map (the o Symtab.curried_lookup vinst) ps; val inst = Symtab.make (parms ~~ ts); val ids' = map (apsnd vinst_names) ids; val wits = List.concat (map (snd o valOf o get_global_registration thy) ids'); @@ -2008,7 +2003,7 @@ |> put_locale name {predicate = predicate, import = import, elems = map (fn e => (e, stamp ())) elems', params = (params_of elemss' |> - map (fn (x, SOME T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss)), + map (fn (x, SOME T) => ((x, T), the (Symtab.curried_lookup syn x))), map #1 (params_of body_elemss)), regs = []} |> pair (elems', body_ctxt) end; @@ -2177,7 +2172,7 @@ NONE => error ("Instance missing for parameter " ^ quote p) | SOME (Free (_, T), t) => (t, T); val d = t |> inst_tab_term (inst, tinst) |> Envir.beta_norm; - in (Symtab.update_new ((p, d), inst), tinst) end; + in (Symtab.curried_update_new (p, d) inst, tinst) end; val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given); (* Note: inst and tinst contain no vars. *) diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Isar/method.ML Thu Sep 01 18:48:50 2005 +0200 @@ -560,7 +560,7 @@ val ((raw_name, _), pos) = Args.dest_src src; val name = NameSpace.intern space raw_name; in - (case Symtab.lookup (meths, name) of + (case Symtab.curried_lookup meths name of NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos) | SOME ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src)) end; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Thu Sep 01 18:48:50 2005 +0200 @@ -125,10 +125,10 @@ fun get_lexicons () = ! global_lexicons; fun get_parsers () = ! global_parsers; -fun get_parser () = Option.map (#2 o #1) o curry Symtab.lookup (get_parsers ()); +fun get_parser () = Option.map (#2 o #1) o Symtab.curried_lookup (get_parsers ()); fun command_tags name = - (case Symtab.lookup (get_parsers (), name) of + (case Symtab.curried_lookup (get_parsers ()) name of SOME (((_, k), _), _) => OuterKeyword.tags_of k | NONE => []); @@ -143,7 +143,7 @@ fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab = (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)); + Symtab.curried_update (name, (((comment, kind), (int_only, parse)), markup)) tab); fun add_parsers parsers = (change_parsers (fold add_parser parsers); diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Sep 01 18:48:50 2005 +0200 @@ -364,18 +364,18 @@ (** default sorts and types **) -fun def_sort ctxt xi = Vartab.lookup (#2 (defaults_of ctxt), xi); +val def_sort = Vartab.curried_lookup o #2 o defaults_of; fun def_type ctxt pattern xi = let val {binds, defs = (types, _, _, _), ...} = rep_context ctxt in - (case Vartab.lookup (types, xi) of + (case Vartab.curried_lookup types xi of NONE => if pattern then NONE - else Vartab.lookup (binds, xi) |> Option.map (TypeInfer.polymorphicT o #2) + else Vartab.curried_lookup binds xi |> Option.map (TypeInfer.polymorphicT o #2) | some => some) end; -fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt), (x, ~1)); +fun default_type ctxt x = Vartab.curried_lookup (#1 (defaults_of ctxt)) (x, ~1); val used_types = #3 o defaults_of; @@ -492,7 +492,7 @@ val binds = binds_of ctxt; fun norm (t as Var (xi, T)) = - (case Vartab.lookup (binds, xi) of + (case Vartab.curried_lookup binds xi of SOME (u, U) => let val env = unifyT ctxt (T, U) handle Type.TUNIFY => @@ -596,24 +596,24 @@ local val ins_types = fold_aterms - (fn Free (x, T) => curry Vartab.update ((x, ~1), T) - | Var v => curry Vartab.update v + (fn Free (x, T) => Vartab.curried_update ((x, ~1), T) + | Var v => Vartab.curried_update v | _ => I); val ins_sorts = fold_types (fold_atyps - (fn TFree (x, S) => curry Vartab.update ((x, ~1), S) - | TVar v => curry Vartab.update v + (fn TFree (x, S) => Vartab.curried_update ((x, ~1), S) + | TVar v => Vartab.curried_update v | _ => I)); val ins_used = fold_term_types (fn t => fold_atyps (fn TFree (x, _) => insert (op =) x | _ => I)); val ins_occs = fold_term_types (fn t => - fold_atyps (fn TFree (x, _) => curry Symtab.update_multi (x, t) | _ => I)); + fold_atyps (fn TFree (x, _) => Symtab.curried_update_multi (x, t) | _ => I)); fun ins_skolem def_ty = fold_rev (fn (x, x') => (case def_ty x' of - SOME T => curry Vartab.update ((x, ~1), T) + SOME T => Vartab.curried_update ((x, ~1), T) | NONE => I)); fun map_defaults f = map_context (fn (syntax, asms, binds, thms, cases, defs) => @@ -632,7 +632,7 @@ |> declare_term_syntax t |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs t occ)) |> map_defaults (fn (types, sorts, used, occ) => - (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes_of ctxt) types, + (ins_skolem (fn x => Vartab.curried_lookup types (x, ~1)) (fixes_of ctxt) types, sorts, used, occ)); end; @@ -690,7 +690,7 @@ val occs_outer = type_occs_of outer; fun add a gen = if Symtab.defined occs_outer a orelse - exists still_fixed (Symtab.lookup_multi (occs_inner, a)) + exists still_fixed (Symtab.curried_lookup_multi occs_inner a) then gen else a :: gen; in fn tfrees => fold add tfrees [] end; @@ -777,7 +777,7 @@ else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T); in map_context (fn (syntax, asms, binds, thms, cases, defs) => - (syntax, asms, Vartab.update (((x, i), (t', T)), binds), thms, cases, defs)) + (syntax, asms, Vartab.curried_update ((x, i), (t', T)) binds, thms, cases, defs)) o declare_term t' end; @@ -935,7 +935,7 @@ val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref; val name = PureThy.name_of_thmref thmref; in - (case Symtab.lookup (tab, name) of + (case Symtab.curried_lookup tab name of SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths) | NONE => from_thy thy xthmref) |> pick name end @@ -990,7 +990,7 @@ let val name = NameSpace.full naming bname; val space' = NameSpace.declare naming name space; - val tab' = Symtab.update ((name, ths), tab); + val tab' = Symtab.curried_update (name, ths) tab; val index' = FactIndex.add (is_known ctxt) (name, ths) index; in (syntax, asms, binds, (naming, (space', tab'), index'), cases, defs) end); diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Isar/term_style.ML --- a/src/Pure/Isar/term_style.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Isar/term_style.ML Thu Sep 01 18:48:50 2005 +0200 @@ -2,7 +2,8 @@ ID: $Id$ Author: Florian Haftmann, TU Muenchen -Styles for terms, to use with the "term_style" and "thm_style" antiquotations. +Styles for terms, to use with the "term_style" and "thm_style" +antiquotations. *) signature TERM_STYLE = @@ -39,12 +40,12 @@ (* accessors *) fun the_style thy name = - (case Symtab.lookup (StyleData.get thy, name) of + (case Symtab.curried_lookup (StyleData.get thy) name of NONE => error ("Unknown antiquote style: " ^ quote name) | SOME (style, _) => style); fun add_style name style thy = - StyleData.map (curry Symtab.update_new (name, (style, stamp ()))) thy + StyleData.map (Symtab.curried_update_new (name, (style, stamp ()))) thy handle Symtab.DUP _ => err_dup_styles [name]; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Syntax/ast.ML Thu Sep 01 18:48:50 2005 +0200 @@ -157,7 +157,7 @@ if a = b then env else raise NO_MATCH | mtch (Variable a) (Constant b) env = if a = b then env else raise NO_MATCH - | mtch ast (Variable x) env = Symtab.update ((x, ast), env) + | mtch ast (Variable x) env = Symtab.curried_update (x, ast) env | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env | mtch _ _ _ = raise NO_MATCH and mtch_lst (ast :: asts) (pat :: pats) env = @@ -189,7 +189,7 @@ val changes = ref 0; fun subst _ (ast as Constant _) = ast - | subst env (Variable x) = the (Symtab.lookup (env, x)) + | subst env (Variable x) = the (Symtab.curried_lookup env x) | subst env (Appl asts) = Appl (map (subst env) asts); fun try_rules ((lhs, rhs) :: pats) ast = diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Syntax/parser.ML Thu Sep 01 18:48:50 2005 +0200 @@ -446,9 +446,9 @@ let (*Get tag for existing nonterminal or create a new one*) fun get_tag nt_count tags nt = - case Symtab.lookup (tags, nt) of + case Symtab.curried_lookup tags nt of SOME tag => (nt_count, tags, tag) - | NONE => (nt_count+1, Symtab.update_new ((nt, nt_count), tags), + | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags, nt_count); (*Convert symbols to the form used by the parser; @@ -523,9 +523,9 @@ (*get existing tag from grammar1 or create a new one*) fun get_tag nt_count tags nt = - case Symtab.lookup (tags, nt) of + case Symtab.curried_lookup tags nt of SOME tag => (nt_count, tags, tag) - | NONE => (nt_count+1, Symtab.update_new ((nt, nt_count), tags), + | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags, nt_count) val ((nt_count1', tags1'), tag_table) = @@ -868,7 +868,7 @@ fun earley prods tags chains startsymbol indata = let - val start_tag = case Symtab.lookup (tags, startsymbol) of + val start_tag = case Symtab.curried_lookup tags startsymbol of SOME tag => tag | NONE => error ("parse: Unknown startsymbol " ^ quote startsymbol); diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Syntax/printer.ML Thu Sep 01 18:48:50 2005 +0200 @@ -248,7 +248,7 @@ val tab = fold f fmts (mode_tab prtabs mode); in AList.update (op =) (mode, tab) prtabs end; -fun extend_prtabs m = change_prtabs (curry Symtab.update_multi) m; +fun extend_prtabs m = change_prtabs Symtab.curried_update_multi m; fun remove_prtabs m = change_prtabs (Symtab.remove_multi (op =)) m; fun merge_prtabs prtabs1 prtabs2 = @@ -330,7 +330,7 @@ (*find matching table entry, or print as prefix / postfix*) fun prnt ([], []) = prefixT tup - | prnt ([], tb :: tbs) = prnt (Symtab.lookup_multi (tb, a), tbs) + | prnt ([], tb :: tbs) = prnt (Symtab.curried_lookup_multi tb a, tbs) | prnt ((pr, n, p') :: prnps, tbs) = if nargs = n then parT (pr, args, p, p') else if nargs > n andalso not type_mode then diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Syntax/syntax.ML Thu Sep 01 18:48:50 2005 +0200 @@ -82,7 +82,7 @@ (* parse (ast) translations *) -fun lookup_tr tab c = Option.map fst (Symtab.lookup (tab, c)); +fun lookup_tr tab c = Option.map fst (Symtab.curried_lookup tab c); fun err_dup_trfuns name cs = error ("More than one " ^ name ^ " for " ^ commas_quote cs); @@ -98,8 +98,8 @@ (* print (ast) translations *) -fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c)); -fun extend_tr'tab trfuns = fold_rev (curry Symtab.update_multi) trfuns; +fun lookup_tr' tab c = map fst (Symtab.curried_lookup_multi tab c); +fun extend_tr'tab trfuns = fold_rev Symtab.curried_update_multi trfuns; fun remove_tr'tab trfuns = fold (Symtab.remove_multi SynExt.eq_trfun) trfuns; fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' SynExt.eq_trfun (tab1, tab2); @@ -147,16 +147,12 @@ type ruletab = (Ast.ast * Ast.ast) list Symtab.table; fun dest_ruletab tab = List.concat (map snd (Symtab.dest tab)); -fun lookup_ruletab tab a = Symtab.lookup_multi (tab, a); (* empty, extend, merge ruletabs *) -val extend_ruletab = - fold_rev (fn r => fn tab => Symtab.update_multi ((Ast.head_of_rule r, r), tab)); - +val extend_ruletab = fold_rev (fn r => Symtab.curried_update_multi (Ast.head_of_rule r, r)); val remove_ruletab = fold (fn r => Symtab.remove_multi (op =) (Ast.head_of_rule r, r)); - fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2); @@ -389,7 +385,7 @@ val asts = read_asts thy is_logtype syn false (SynExt.typ_to_nonterm ty) str; in SynTrans.asts_to_terms thy (lookup_tr parse_trtab) - (map (Ast.normalize_ast (lookup_ruletab parse_ruletab)) asts) + (map (Ast.normalize_ast (Symtab.curried_lookup_multi parse_ruletab)) asts) end; @@ -473,7 +469,7 @@ in prt_t thy curried prtabs (lookup_tr' print_ast_trtab) (lookup_tokentr tokentrtab (! print_mode)) - (Ast.normalize_ast (lookup_ruletab print_ruletab) ast) + (Ast.normalize_ast (Symtab.curried_lookup_multi print_ruletab) ast) end; val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Thy/html.ML Thu Sep 01 18:48:50 2005 +0200 @@ -205,7 +205,7 @@ fun output_sym s = if Symbol.is_raw s then (1.0, Symbol.decode_raw s) else - (case Symtab.lookup (html_syms, s) of SOME x => x + (case Symtab.curried_lookup html_syms s of SOME x => x | NONE => (real (size s), translate_string escape s)); fun output_sub s = apsnd (enclose "" "") (output_sym s); diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Thy/present.ML Thu Sep 01 18:48:50 2005 +0200 @@ -172,13 +172,13 @@ fun init_theory_info name info = change_browser_info (fn (theories, files, tex_index, html_index, graph) => - (Symtab.update ((name, info), theories), files, tex_index, html_index, graph)); + (Symtab.curried_update (name, info) theories, files, tex_index, html_index, graph)); fun change_theory_info name f = change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) => - (case Symtab.lookup (theories, name) of + (case Symtab.curried_lookup theories name of NONE => (warning ("Browser info: cannot access theory document " ^ quote name); info) - | SOME info => (Symtab.update ((name, map_theory_info f info), theories), files, + | SOME info => (Symtab.curried_update (name, map_theory_info f info) theories, files, tex_index, html_index, graph))); diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Thy/thm_database.ML --- a/src/Pure/Thy/thm_database.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Thy/thm_database.ML Thu Sep 01 18:48:50 2005 +0200 @@ -88,7 +88,7 @@ fun result prfx bname = if (prfx = "" orelse is_ml_identifier prfx) andalso is_ml_identifier bname andalso NameSpace.intern space xname = name then - SOME (prfx, (bname, xname, length (the (Symtab.lookup (thms, name))) = 1)) + SOME (prfx, (bname, xname, length (the (Symtab.curried_lookup thms name)) = 1)) else NONE; val names = NameSpace.unpack name; in diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/Thy/thy_parse.ML --- a/src/Pure/Thy/thy_parse.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/Thy/thy_parse.ML Thu Sep 01 18:48:50 2005 +0200 @@ -469,7 +469,7 @@ end; fun sect tab ((Keyword, s, n) :: toks) = - (case Symtab.lookup (tab, s) of + (case Symtab.curried_lookup tab s of SOME parse => !! parse toks | NONE => syn_err "section" s n) | sect _ ((_, s, n) :: _) = syn_err "section" s n diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/axclass.ML Thu Sep 01 18:48:50 2005 +0200 @@ -153,7 +153,7 @@ (* get and put data *) -fun lookup_axclass_info thy c = Symtab.lookup (AxclassesData.get thy, c); +val lookup_axclass_info = Symtab.curried_lookup o AxclassesData.get; fun get_axclass_info thy c = (case lookup_axclass_info thy c of @@ -161,7 +161,7 @@ | SOME info => info); fun put_axclass_info c info thy = - thy |> AxclassesData.put (Symtab.update ((c, info), AxclassesData.get thy)); + thy |> AxclassesData.put (Symtab.curried_update (c, info) (AxclassesData.get thy)); (* class_axms *) diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/compress.ML --- a/src/Pure/compress.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/compress.ML Thu Sep 01 18:48:50 2005 +0200 @@ -42,11 +42,11 @@ let val typs = #1 (CompressData.get thy); fun compress T = - (case Typtab.lookup (! typs, T) of + (case Typtab.curried_lookup (! typs) T of SOME T' => T' | NONE => let val T' = (case T of Type (a, Ts) => Type (a, map compress Ts) | _ => T) - in change typs (curry Typtab.update (T', T')); T' end); + in change typs (Typtab.curried_update (T', T')); T' end); in compress end; @@ -58,9 +58,9 @@ fun compress (t $ u) = compress t $ compress u | compress (Abs (a, T, t)) = Abs (a, T, compress t) | compress t = - (case Termtab.lookup (! terms, t) of + (case Termtab.curried_lookup (! terms) t of SOME t' => t' - | NONE => (change terms (curry Termtab.update (t, t)); t)); + | NONE => (change terms (Termtab.curried_update (t, t)); t)); in compress o map_term_types (typ thy) end; end; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/context.ML --- a/src/Pure/context.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/context.ML Thu Sep 01 18:48:50 2005 +0200 @@ -121,7 +121,7 @@ val kinds = ref (Inttab.empty: kind Inttab.table); fun invoke meth_name meth_fn k = - (case Inttab.lookup (! kinds, k) of + (case Inttab.curried_lookup (! kinds) k of SOME kind => meth_fn kind |> transform_failure (fn exn => DATA_FAIL (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed")) | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k)); @@ -140,7 +140,7 @@ val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge}; val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () => warning ("Duplicate declaration of theory data " ^ quote name)); - val _ = kinds := Inttab.update ((k, kind), ! kinds); + val _ = change kinds (Inttab.curried_update (k, kind)); in k end; val copy_data = Inttab.map' invoke_copy; @@ -256,7 +256,7 @@ 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); + else Inttab.curried_update id ids; fun check_insert intermediate id (ids, iids) = let val ids' = check_ins id ids and iids' = check_ins id iids @@ -423,12 +423,12 @@ val declare = declare_theory_data; fun get k dest thy = - (case Inttab.lookup (#theory (data_of thy), k) of + (case Inttab.curried_lookup (#theory (data_of thy)) k of SOME x => (dest x handle Match => error ("Failed to access theory data " ^ quote (invoke_name k))) | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k))); -fun put k mk x = modify_thy (map_theory (curry Inttab.update (k, mk x))); +fun put k mk x = modify_thy (map_theory (Inttab.curried_update (k, mk x))); fun init k = put k I (invoke_empty k); end; @@ -525,7 +525,7 @@ val kinds = ref (Inttab.empty: kind Inttab.table); fun invoke meth_name meth_fn k = - (case Inttab.lookup (! kinds, k) of + (case Inttab.curried_lookup (! kinds) k of SOME kind => meth_fn kind |> transform_failure (fn exn => DATA_FAIL (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed")) | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k)); @@ -549,18 +549,18 @@ val kind = {name = name, init = init}; val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () => warning ("Duplicate declaration of proof data " ^ quote name)); - val _ = kinds := Inttab.update ((k, kind), ! kinds); + val _ = change kinds (Inttab.curried_update (k, kind)); in k end; -fun init k = modify_thy (map_proof (curry Inttab.update (k, ()))); +fun init k = modify_thy (map_proof (Inttab.curried_update (k, ()))); fun get k dest prf = - (case Inttab.lookup (data_of_proof prf, k) of + (case Inttab.curried_lookup (data_of_proof prf) k of SOME x => (dest x handle Match => error ("Failed to access proof data " ^ quote (invoke_name k))) | NONE => error ("Uninitialized proof data " ^ quote (invoke_name k))); -fun put k mk x = map_prf (curry Inttab.update (k, mk x)); +fun put k mk x = map_prf (Inttab.curried_update (k, mk x)); end; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/fact_index.ML --- a/src/Pure/fact_index.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/fact_index.ML Thu Sep 01 18:48:50 2005 +0200 @@ -55,7 +55,7 @@ fun add pred (name, ths) (Index {next, facts, consts, frees}) = let - fun upd a tab = Symtab.update_multi ((a, (next, (name, ths))), tab); + fun upd a = Symtab.curried_update_multi (a, (next, (name, ths))); val (cs, xs) = fold (index_thm pred) ths ([], []); in Index {next = next + 1, facts = (name, ths) :: facts, @@ -74,7 +74,7 @@ fun find idx ([], []) = facts idx | find (Index {consts, frees, ...}) (cs, xs) = - (map (curry Symtab.lookup_multi consts) cs @ - map (curry Symtab.lookup_multi frees) xs) |> intersects |> map #2; + (map (Symtab.curried_lookup_multi consts) cs @ + map (Symtab.curried_lookup_multi frees) xs) |> intersects |> map #2; end; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/net.ML --- a/src/Pure/net.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/net.ML Thu Sep 01 18:48:50 2005 +0200 @@ -94,8 +94,8 @@ Net{comb=comb, var=ins1(keys,var), atoms=atoms} | ins1 (AtomK a :: keys, Net{comb,var,atoms}) = let - val net' = if_none (Symtab.lookup (atoms, a)) empty; - val atoms' = Symtab.update ((a, ins1(keys,net')), atoms); + val net' = if_none (Symtab.curried_lookup atoms a) empty; + val atoms' = Symtab.curried_update (a, ins1 (keys, net')) atoms; in Net{comb=comb, var=var, atoms=atoms'} end in ins1 (keys,net) end; @@ -126,12 +126,12 @@ newnet{comb=comb, var=del1(keys,var), atoms=atoms} | del1 (AtomK a :: keys, Net{comb,var,atoms}) = let val atoms' = - (case Symtab.lookup (atoms, a) of + (case Symtab.curried_lookup atoms a of NONE => raise DELETE | SOME net' => (case del1 (keys, net') of Leaf [] => Symtab.delete a atoms - | net'' => Symtab.update ((a, net''), atoms))) + | net'' => Symtab.curried_update (a, net'') atoms)) in newnet{comb=comb, var=var, atoms=atoms'} end in del1 (keys,net) end; @@ -143,7 +143,7 @@ exception ABSENT; fun the_atom atoms a = - (case Symtab.lookup (atoms, a) of + (case Symtab.curried_lookup atoms a of NONE => raise ABSENT | SOME net => net); @@ -222,7 +222,7 @@ subtr comb1 comb2 #> subtr var1 var2 #> Symtab.fold (fn (a, net) => - subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2 + subtr (if_none (Symtab.curried_lookup atoms1 a) emptynet) net) atoms2 in subtr net1 net2 [] end; fun entries net = subtract (K false) empty net; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/pattern.ML --- a/src/Pure/pattern.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/pattern.ML Thu Sep 01 18:48:50 2005 +0200 @@ -357,7 +357,7 @@ if loose_bvar(t,0) then raise MATCH else (case Envir.lookup' (insts, (ixn, T)) of NONE => (typ_match thy (tyinsts, (T, fastype_of t)), - Vartab.update_new ((ixn, (T, t)), insts)) + Vartab.curried_update_new (ixn, (T, t)) insts) | SOME u => if t aeconv u then instsp else raise MATCH) | (Free (a,T), Free (b,U)) => if a=b then (typ_match thy (tyinsts,(T,U)), insts) else raise MATCH @@ -378,11 +378,11 @@ fun match_bind(itms,binders,ixn,T,is,t) = let val js = loose_bnos t in if null is - then if null js then Vartab.update_new ((ixn, (T, t)), itms) else raise MATCH + then if null js then Vartab.curried_update_new (ixn, (T, t)) itms else raise MATCH else if js subset_int is then let val t' = if downto0(is,length binders - 1) then t else mapbnd (idx is) t - in Vartab.update_new ((ixn, (T, mkabs (binders, is, t'))), itms) end + in Vartab.curried_update_new (ixn, (T, mkabs (binders, is, t'))) itms end else raise MATCH end; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/proof_general.ML Thu Sep 01 18:48:50 2005 +0200 @@ -811,11 +811,11 @@ fun get_keywords_classification_table () = case (!keywords_classification_table) of - SOME t => t - | NONE => (let - val tab = Library.foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab)) - (Symtab.empty,OuterSyntax.dest_parsers()) - in (keywords_classification_table := SOME tab; tab) end) + SOME t => t + | NONE => (let + val tab = fold (fn (c, _, k, _) => Symtab.curried_update (c, k)) + (OuterSyntax.dest_parsers ()) Symtab.empty; + in (keywords_classification_table := SOME tab; tab) end) @@ -959,7 +959,7 @@ fun xmls_of_transition (name,str,toks) = let - val classification = Symtab.lookup (get_keywords_classification_table(),name) + val classification = Symtab.curried_lookup (get_keywords_classification_table ()) name in case classification of SOME k => (xmls_of_kind k (name,toks,str)) | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *) diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/proofterm.ML Thu Sep 01 18:48:50 2005 +0200 @@ -143,10 +143,10 @@ | oras_of (prf % _) = oras_of prf | oras_of (prf1 %% prf2) = oras_of prf1 #> oras_of prf2 | oras_of (PThm ((name, _), prf, prop, _)) = (fn tabs as (thms, oras) => - case Symtab.lookup (thms, name) of - NONE => oras_of prf (Symtab.update ((name, [prop]), thms), oras) + case Symtab.curried_lookup thms name of + NONE => oras_of prf (Symtab.curried_update (name, [prop]) thms, oras) | SOME ps => if prop mem ps then tabs else - oras_of prf (Symtab.update ((name, prop::ps), thms), oras)) + oras_of prf (Symtab.curried_update (name, prop::ps) thms, oras)) | oras_of (Oracle (s, prop, _)) = apsnd (OrdList.insert string_term_ord (s, prop)) | oras_of (MinProof (thms, _, oras)) = @@ -162,10 +162,10 @@ | thms_of_proof (prf1 %% prf2) = thms_of_proof prf1 #> thms_of_proof prf2 | thms_of_proof (prf % _) = thms_of_proof prf | thms_of_proof (prf' as PThm ((s, _), prf, prop, _)) = (fn tab => - case Symtab.lookup (tab, s) of - NONE => thms_of_proof prf (Symtab.update ((s, [(prop, prf')]), tab)) + case Symtab.curried_lookup tab s of + NONE => thms_of_proof prf (Symtab.curried_update (s, [(prop, prf')]) tab) | SOME ps => if exists (equal prop o fst) ps then tab else - thms_of_proof prf (Symtab.update ((s, (prop, prf')::ps), tab))) + thms_of_proof prf (Symtab.curried_update (s, (prop, prf')::ps) tab)) | thms_of_proof (MinProof (prfs, _, _)) = fold (thms_of_proof o proof_of_min_thm) prfs | thms_of_proof _ = I; @@ -173,7 +173,7 @@ | axms_of_proof (AbsP (_, _, prf)) = axms_of_proof prf | axms_of_proof (prf1 %% prf2) = axms_of_proof prf1 #> axms_of_proof prf2 | axms_of_proof (prf % _) = axms_of_proof prf - | axms_of_proof (prf as PAxm (s, _, _)) = curry Symtab.update (s, prf) + | axms_of_proof (prf as PAxm (s, _, _)) = Symtab.curried_update (s, prf) | axms_of_proof (MinProof (_, prfs, _)) = fold (axms_of_proof o proof_of_min_axm) prfs | axms_of_proof _ = I; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/pure_thy.ML Thu Sep 01 18:48:50 2005 +0200 @@ -208,8 +208,8 @@ val (space, thms) = #theorems (get_theorems thy); in fn name => - Option.map (map (Thm.transfer (Theory.deref thy_ref))) (*dynamic identity*) - (Symtab.lookup (thms, NameSpace.intern space name)) (*static content*) + Option.map (map (Thm.transfer (Theory.deref thy_ref))) (*dynamic identity*) + (Symtab.curried_lookup thms (NameSpace.intern space name)) (*static content*) end; fun get_thms_closure thy = @@ -309,10 +309,10 @@ val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms)); val r as ref {theorems = (space, theorems), index} = get_theorems_ref thy'; val space' = Sign.declare_name thy' name space; - val theorems' = Symtab.update ((name, thms'), theorems); + val theorems' = Symtab.curried_update (name, thms') theorems; val index' = FactIndex.add (K false) (name, thms') index; in - (case Symtab.lookup (theorems, name) of + (case Symtab.curried_lookup theorems name of NONE => () | SOME thms'' => if Thm.eq_thms (thms', thms'') then warn_same name diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/sign.ML Thu Sep 01 18:48:50 2005 +0200 @@ -282,8 +282,8 @@ fun const_constraint thy c = let val ((_, consts), constraints) = #consts (rep_sg thy) in - (case Symtab.lookup (constraints, c) of - NONE => Option.map #1 (Symtab.lookup (consts, c)) + (case Symtab.curried_lookup constraints c of + NONE => Option.map #1 (Symtab.curried_lookup consts c) | some => some) end; @@ -291,7 +291,7 @@ (case const_constraint thy c of SOME T => T | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], [])); -fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#1 (#consts (rep_sg thy))), c)); +val const_type = Option.map #1 oo (Symtab.curried_lookup o #2 o #1 o #consts o rep_sg); fun the_const_type thy c = (case const_type thy c of SOME T => T @@ -514,7 +514,7 @@ fun read_tyname thy raw_c = let val c = intern_type thy raw_c in - (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy))), c) of + (case Symtab.curried_lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT) | _ => error ("Undeclared type constructor: " ^ quote c)) end; @@ -714,7 +714,7 @@ handle TYPE (msg, _, _) => error msg; val _ = cert_term thy (Const (c, T)) handle TYPE (msg, _, _) => error msg; - in thy |> map_consts (apsnd (curry Symtab.update (c, T))) end; + in thy |> map_consts (apsnd (Symtab.curried_update (c, T))) end; val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort); val add_const_constraint_i = gen_add_constraint (K I) certify_typ; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/sorts.ML Thu Sep 01 18:48:50 2005 +0200 @@ -180,7 +180,7 @@ fun mg_domain (classes, arities) a S = let fun dom c = - (case AList.lookup (op =) (Symtab.lookup_multi (arities, a)) c of + (case AList.lookup (op =) (Symtab.curried_lookup_multi arities a) c of NONE => raise DOMAIN (a, c) | SOME Ss => Ss); fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss); diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/thm.ML Thu Sep 01 18:48:50 2005 +0200 @@ -524,7 +524,7 @@ fun get_axiom_i theory name = let fun get_ax thy = - Symtab.lookup (#2 (#axioms (Theory.rep_theory thy)), name) + Symtab.curried_lookup (#2 (#axioms (Theory.rep_theory thy))) name |> Option.map (fn prop => Thm {thy_ref = Theory.self_ref thy, der = Pt.infer_derivs' I (false, Pt.axm_proof name prop), @@ -1482,7 +1482,7 @@ fun invoke_oracle_i thy1 name = let val oracle = - (case Symtab.lookup (#2 (#oracles (Theory.rep_theory thy1)), name) of + (case Symtab.curried_lookup (#2 (#oracles (Theory.rep_theory thy1))) name of NONE => raise THM ("Unknown oracle: " ^ name, 0, []) | SOME (f, _) => f); val thy_ref1 = Theory.self_ref thy1; diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/type.ML --- a/src/Pure/type.ML Thu Sep 01 16:19:02 2005 +0200 +++ b/src/Pure/type.ML Thu Sep 01 18:48:50 2005 +0200 @@ -167,7 +167,7 @@ val Ts' = map cert Ts; fun nargs n = if length Ts <> n then err (bad_nargs c) else (); in - (case Symtab.lookup (types, c) of + (case Symtab.curried_lookup types c of SOME (LogicalType n, _) => (nargs n; Type (c, Ts')) | SOME (Abbreviation (vs, U, syn), _) => (nargs (length vs); if syn then check_syntax c else (); @@ -284,7 +284,7 @@ [TVar (ixn, S), TVar (ixn, S')], []); fun lookup (tye, (ixn, S)) = - (case Vartab.lookup (tye, ixn) of + (case Vartab.curried_lookup tye ixn of NONE => NONE | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S'); @@ -298,7 +298,7 @@ fun match (TVar (v, S), T) subs = (case lookup (subs, (v, S)) of NONE => - if of_sort tsig (T, S) then Vartab.update_new ((v, (S, T)), subs) + if of_sort tsig (T, S) then Vartab.curried_update_new (v, (S, T)) subs else raise TYPE_MATCH | SOME U => if U = T then subs else raise TYPE_MATCH) | match (Type (a, Ts), Type (b, Us)) subs = @@ -317,7 +317,7 @@ (*purely structural matching*) fun raw_match (TVar (v, S), T) subs = (case lookup (subs, (v, S)) of - NONE => Vartab.update_new ((v, (S, T)), subs) + NONE => Vartab.curried_update_new (v, (S, T)) subs | SOME U => if U = T then subs else raise TYPE_MATCH) | raw_match (Type (a, Ts), Type (b, Us)) subs = if a <> b then raise TYPE_MATCH @@ -366,8 +366,8 @@ fun meet (_, []) tye = tye | meet (TVar (xi, S'), S) tye = if Sorts.sort_le classes (S', S) then tye - else Vartab.update_new ((xi, (S', - gen_tyvar (Sorts.inter_sort classes (S', S)))), tye) + else Vartab.curried_update_new + (xi, (S', gen_tyvar (Sorts.inter_sort classes (S', S)))) tye | meet (TFree (_, S'), S) tye = if Sorts.sort_le classes (S', S) then tye else raise TUNIFY @@ -381,19 +381,19 @@ if eq_ix (v, w) then if S1 = S2 then tye else tvar_clash v S1 S2 else if Sorts.sort_le classes (S1, S2) then - Vartab.update_new ((w, (S2, T)), tye) + Vartab.curried_update_new (w, (S2, T)) tye else if Sorts.sort_le classes (S2, S1) then - Vartab.update_new ((v, (S1, U)), tye) + Vartab.curried_update_new (v, (S1, U)) tye else let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in - Vartab.update_new ((v, (S1, S)), Vartab.update_new ((w, (S2, S)), tye)) + Vartab.curried_update_new (v, (S1, S)) (Vartab.curried_update_new (w, (S2, S)) tye) end | (TVar (v, S), T) => if occurs v tye T then raise TUNIFY - else meet (T, S) (Vartab.update_new ((v, (S, T)), tye)) + else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye) | (T, TVar (v, S)) => if occurs v tye T then raise TUNIFY - else meet (T, S) (Vartab.update_new ((v, (S, T)), tye)) + else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye) | (Type (a, Ts), Type (b, Us)) => if a <> b then raise TUNIFY else unifs (Ts, Us) tye @@ -408,13 +408,13 @@ (T as TVar (v, S1), U as TVar (w, S2)) => if eq_ix (v, w) then if S1 = S2 then tye else tvar_clash v S1 S2 - else Vartab.update_new ((w, (S2, T)), tye) + else Vartab.curried_update_new (w, (S2, T)) tye | (TVar (v, S), T) => if occurs v tye T then raise TUNIFY - else Vartab.update_new ((v, (S, T)), tye) + else Vartab.curried_update_new (v, (S, T)) tye | (T, TVar (v, S)) => if occurs v tye T then raise TUNIFY - else Vartab.update_new ((v, (S, T)), tye) + else Vartab.curried_update_new (v, (S, T)) tye | (Type (a, Ts), Type (b, Us)) => if a <> b then raise TUNIFY else raw_unifys (Ts, Us) tye @@ -476,9 +476,9 @@ fun insert_arities pp classes (t, ars) arities = let val ars' = - Symtab.lookup_multi (arities, t) + Symtab.curried_lookup_multi arities t |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars) - in Symtab.update ((t, ars'), arities) end; + in Symtab.curried_update (t, ars') arities end; fun insert_table pp classes = Symtab.fold (fn (t, ars) => insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars)); @@ -488,7 +488,7 @@ fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) => let fun prep (t, Ss, S) = - (case Symtab.lookup (#2 types, t) of + (case Symtab.curried_lookup (#2 types) t of SOME (LogicalType n, _) => if length Ss = n then (t, map (cert_sort tsig) Ss, cert_sort tsig S) @@ -591,18 +591,18 @@ val c' = NameSpace.full naming c; val space' = NameSpace.declare naming c' space; val types' = - (case Symtab.lookup (types, c') of + (case Symtab.curried_lookup types c' of SOME (decl', _) => err_in_decls c' decl decl' - | NONE => Symtab.update ((c', (decl, stamp ())), types)); + | NONE => Symtab.curried_update (c', (decl, stamp ())) types); in (space', types') end; -fun the_decl (_, types) c = fst (the (Symtab.lookup (types, c))); +fun the_decl (_, types) = fst o the o Symtab.curried_lookup types; fun change_types f = map_tsig (fn (classes, default, types, arities) => (classes, default, f types, arities)); fun syntactic types (Type (c, Ts)) = - (case Symtab.lookup (types, c) of SOME (Nonterminal, _) => true | _ => false) + (case Symtab.curried_lookup types c of SOME (Nonterminal, _) => true | _ => false) orelse exists (syntactic types) Ts | syntactic _ _ = false;