# HG changeset patch # User wenzelm # Date 1126797416 -7200 # Node ID e26cb20ef0cc380198e5617e3bc3f8bb8d149fc4 # Parent 664434175578f2b87822565452da78407ece35ee TableFun/Symtab: curried lookup and update; diff -r 664434175578 -r e26cb20ef0cc TFL/casesplit.ML --- a/TFL/casesplit.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/TFL/casesplit.ML Thu Sep 15 17:16:56 2005 +0200 @@ -126,7 +126,7 @@ ("Free type: " ^ s) | TVar((s,i),_) => raise ERROR_MESSAGE ("Free variable: " ^ s) - val dt = case Symtab.curried_lookup dtypestab ty_str + val dt = case Symtab.lookup dtypestab ty_str of SOME dt => dt | NONE => raise ERROR_MESSAGE ("Not a Datatype: " ^ ty_str) in diff -r 664434175578 -r e26cb20ef0cc TFL/thry.ML --- a/TFL/thry.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/TFL/thry.ML Thu Sep 15 17:16:56 2005 +0200 @@ -59,7 +59,7 @@ * Get information about datatypes *---------------------------------------------------------------------------*) -val get_info = Symtab.curried_lookup o DatatypePackage.get_datatypes; +val get_info = Symtab.lookup o DatatypePackage.get_datatypes; fun match_info thy tname = case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of diff -r 664434175578 -r e26cb20ef0cc src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Import/hol4rews.ML Thu Sep 15 17:16:56 2005 +0200 @@ -110,12 +110,12 @@ structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs); fun get_segment2 thyname thy = - Symtab.curried_lookup (HOL4Imports.get thy) thyname + Symtab.lookup (HOL4Imports.get thy) thyname fun set_segment thyname segname thy = let val imps = HOL4Imports.get thy - val imps' = Symtab.curried_update_new (thyname,segname) imps + val imps' = Symtab.update_new (thyname,segname) imps in HOL4Imports.put imps' thy end @@ -273,7 +273,7 @@ let val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm) val curmaps = HOL4Maps.get thy - val newmaps = StringPair.update_new(((bthy,bthm),NONE),curmaps) + val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps val upd_thy = HOL4Maps.put newmaps thy in upd_thy @@ -291,19 +291,19 @@ fun add_hol4_move bef aft thy = let val curmoves = HOL4Moves.get thy - val newmoves = Symtab.curried_update_new (bef, aft) curmoves + val newmoves = Symtab.update_new (bef, aft) curmoves in HOL4Moves.put newmoves thy end fun get_hol4_move bef thy = - Symtab.curried_lookup (HOL4Moves.get thy) bef + Symtab.lookup (HOL4Moves.get thy) bef fun follow_name thmname thy = let val moves = HOL4Moves.get thy fun F thmname = - case Symtab.curried_lookup moves thmname of + case Symtab.lookup moves thmname of SOME name => F name | NONE => thmname in @@ -313,19 +313,19 @@ fun add_hol4_cmove bef aft thy = let val curmoves = HOL4CMoves.get thy - val newmoves = Symtab.curried_update_new (bef, aft) curmoves + val newmoves = Symtab.update_new (bef, aft) curmoves in HOL4CMoves.put newmoves thy end fun get_hol4_cmove bef thy = - Symtab.curried_lookup (HOL4CMoves.get thy) bef + Symtab.lookup (HOL4CMoves.get thy) bef fun follow_cname thmname thy = let val moves = HOL4CMoves.get thy fun F thmname = - case Symtab.curried_lookup moves thmname of + case Symtab.lookup moves thmname of SOME name => F name | NONE => thmname in @@ -337,7 +337,7 @@ val isathm = follow_name isathm thy val _ = message ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm) val curmaps = HOL4Maps.get thy - val newmaps = StringPair.update_new(((bthy,bthm),SOME isathm),curmaps) + val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps val upd_thy = HOL4Maps.put newmaps thy in upd_thy @@ -347,14 +347,14 @@ let val maps = HOL4TypeMaps.get thy in - StringPair.lookup(maps,(bthy,tycon)) + StringPair.lookup maps (bthy,tycon) end fun get_hol4_mapping bthy bthm thy = let val curmaps = HOL4Maps.get thy in - StringPair.lookup(curmaps,(bthy,bthm)) + StringPair.lookup curmaps (bthy,bthm) end; fun add_hol4_const_mapping bthy bconst internal isaconst thy = @@ -366,7 +366,7 @@ else thy val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) val curmaps = HOL4ConstMaps.get thy - val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst,NONE)),curmaps) + val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps val upd_thy = HOL4ConstMaps.put newmaps thy in upd_thy @@ -376,7 +376,7 @@ let val currens = HOL4Rename.get thy val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname) - val newrens = StringPair.update_new(((bthy,bconst),newname),currens) + val newrens = StringPair.update_new ((bthy,bconst),newname) currens val upd_thy = HOL4Rename.put newrens thy in upd_thy @@ -386,7 +386,7 @@ let val currens = HOL4Rename.get thy in - StringPair.lookup(currens,(bthy,bconst)) + StringPair.lookup currens (bthy,bconst) end; fun get_hol4_const_mapping bthy bconst thy = @@ -396,7 +396,7 @@ | NONE => bconst val maps = HOL4ConstMaps.get thy in - StringPair.lookup(maps,(bthy,bconst)) + StringPair.lookup maps (bthy,bconst) end fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy = @@ -408,7 +408,7 @@ else thy val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) val curmaps = HOL4ConstMaps.get thy - val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst,SOME typ)),curmaps) + val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps val upd_thy = HOL4ConstMaps.put newmaps thy in upd_thy @@ -418,8 +418,8 @@ let val curmaps = HOL4TypeMaps.get thy val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) - val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst)),curmaps) - handle x => let val (internal, isaconst') = the (StringPair.lookup (curmaps, (bthy, bconst))) in + val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps + handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end val upd_thy = HOL4TypeMaps.put newmaps thy in @@ -431,7 +431,7 @@ val thmname = Sign.full_name (sign_of thy) bthm val _ = message ("Add pending " ^ bthy ^ "." ^ bthm) val curpend = HOL4Pending.get thy - val newpend = StringPair.update_new(((bthy,bthm),hth),curpend) + val newpend = StringPair.update_new ((bthy,bthm),hth) curpend val upd_thy = HOL4Pending.put newpend thy val thy' = case opt_get_output_thy upd_thy of "" => add_hol4_mapping bthy bthm thmname upd_thy @@ -450,14 +450,14 @@ let val isathms = HOL4Thms.get thy in - StringPair.lookup (isathms,(thyname,thmname)) + StringPair.lookup isathms (thyname,thmname) end fun add_hol4_theorem thyname thmname hth thy = let val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname) val isathms = HOL4Thms.get thy - val isathms' = StringPair.update_new (((thyname,thmname),hth),isathms) + val isathms' = StringPair.update_new ((thyname,thmname),hth) isathms val thy' = HOL4Thms.put isathms' thy in thy' @@ -692,14 +692,14 @@ let val maps = HOL4DefMaps.get thy in - StringPair.lookup(maps,(thyname,const)) + StringPair.lookup maps (thyname,const) end fun add_defmap thyname const defname thy = let val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname) val maps = HOL4DefMaps.get thy - val maps' = StringPair.update_new(((thyname,const),defname),maps) + val maps' = StringPair.update_new ((thyname,const),defname) maps val thy' = HOL4DefMaps.put maps' thy in thy' @@ -710,7 +710,7 @@ val maps = HOL4DefMaps.get thy fun F dname = (dname,add_defmap thyname name dname thy) in - case StringPair.lookup(maps,(thyname,name)) of + case StringPair.lookup maps (thyname,name) of SOME thmname => (thmname,thy) | NONE => let diff -r 664434175578 -r e26cb20ef0cc src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Import/proof_kernel.ML Thu Sep 15 17:16:56 2005 +0200 @@ -420,7 +420,7 @@ val name = intern_const_name Thy Nam thy val cmaps = HOL4ConstMaps.get thy in - case StringPair.lookup(cmaps,(Thy,Nam)) of + case StringPair.lookup cmaps (Thy,Nam) of SOME(_,_,SOME ty) => Const(name,ty) | _ => get_const (sign_of thy) Thy name end @@ -1081,7 +1081,7 @@ let val pending = HOL4Pending.get thy in - case StringPair.lookup (pending,(thyname,thmname)) of + case StringPair.lookup pending (thyname,thmname) of SOME hth => SOME (HOLThm hth) | NONE => NONE end diff -r 664434175578 -r e26cb20ef0cc src/HOL/Matrix/cplex/CplexMatrixConverter.ML --- a/src/HOL/Matrix/cplex/CplexMatrixConverter.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Matrix/cplex/CplexMatrixConverter.ML Thu Sep 15 17:16:56 2005 +0200 @@ -57,14 +57,14 @@ let fun build_naming index i2s s2i [] = (index, i2s, s2i) | build_naming index i2s s2i (cplexBounds (cplexNeg cplexInf, cplexLeq, cplexVar v, cplexLeq, cplexInf)::bounds) - = build_naming (index+1) (Inttab.curried_update (index, v) i2s) (Symtab.curried_update_new (v, index) s2i) bounds + = build_naming (index+1) (Inttab.update (index, v) i2s) (Symtab.update_new (v, index) s2i) bounds | build_naming _ _ _ _ = raise (Converter "nonfree bound") val (varcount, i2s_tab, s2i_tab) = build_naming 0 Inttab.empty Symtab.empty bounds - fun i2s i = case Inttab.curried_lookup i2s_tab i of NONE => raise (Converter "index not found") + fun i2s i = case Inttab.lookup i2s_tab i of NONE => raise (Converter "index not found") | SOME n => n - fun s2i s = case Symtab.curried_lookup s2i_tab s of NONE => raise (Converter ("name not found: "^s)) + fun s2i s = case Symtab.lookup s2i_tab s of NONE => raise (Converter ("name not found: "^s)) | SOME i => i fun num2str positive (cplexNeg t) = num2str (not positive) t | num2str positive (cplexNum num) = if positive then num else "-"^num diff -r 664434175578 -r e26cb20ef0cc src/HOL/Matrix/cplex/Cplex_tools.ML --- a/src/HOL/Matrix/cplex/Cplex_tools.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Thu Sep 15 17:16:56 2005 +0200 @@ -725,7 +725,7 @@ val emptyset = Symtab.empty -fun singleton v = Symtab.update ((v, ()), emptyset) +fun singleton v = Symtab.update (v, ()) emptyset fun merge a b = Symtab.merge (op =) (a, b) diff -r 664434175578 -r e26cb20ef0cc src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Thu Sep 15 17:16:56 2005 +0200 @@ -212,7 +212,7 @@ else if (approx_value_term 1 I str) = zero_interval then vector else - Inttab.curried_update (index, str) vector + Inttab.update (index, str) vector fun set_vector matrix index vector = if index < 0 then @@ -220,7 +220,7 @@ else if Inttab.is_empty vector then matrix else - Inttab.curried_update (index, vector) matrix + Inttab.update (index, vector) matrix val empty_matrix = Inttab.empty val empty_vector = Inttab.empty @@ -232,9 +232,9 @@ fun transpose_matrix matrix = let fun upd m j i x = - case Inttab.curried_lookup m j of - SOME v => Inttab.curried_update (j, Inttab.curried_update (i, x) v) m - | NONE => Inttab.curried_update (j, Inttab.curried_update (i, x) Inttab.empty) m + case Inttab.lookup m j of + SOME v => Inttab.update (j, Inttab.update (i, x) v) m + | NONE => Inttab.update (j, Inttab.update (i, x) Inttab.empty) m fun updv j (m, (i, s)) = upd m i j s @@ -258,7 +258,7 @@ fun nameof i = let val s = "x"^(Int.toString i) - val _ = change ytable (Inttab.curried_update (i, s)) + val _ = change ytable (Inttab.update (i, s)) in s end @@ -281,7 +281,7 @@ fun mk_constr index vector c = let - val s = case Inttab.curried_lookup c index of SOME s => s | NONE => "0" + val s = case Inttab.lookup c index of SOME s => s | NONE => "0" val (p, s) = split_numstr s val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s) in @@ -334,7 +334,7 @@ fun mk_constr index vector c = let - val s = case Inttab.curried_lookup c index of SOME s => s | NONE => "0" + val s = case Inttab.lookup c index of SOME s => s | NONE => "0" val (p, s) = split_numstr s val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s) in @@ -358,7 +358,7 @@ val count = ref 0 fun app (v, (i, s)) = if (!count < size) then - (count := !count +1 ; Inttab.curried_update (i,s) v) + (count := !count +1 ; Inttab.update (i,s) v) else v in @@ -368,18 +368,18 @@ fun cut_matrix vfilter vsize m = let fun app (m, (i, v)) = - if Inttab.curried_lookup vfilter i = NONE then + if Inttab.lookup vfilter i = NONE then m else case vsize of - NONE => Inttab.curried_update (i,v) m - | SOME s => Inttab.curried_update (i, cut_vector s v) m + NONE => Inttab.update (i,v) m + | SOME s => Inttab.update (i, cut_vector s v) m in Inttab.foldl app (empty_matrix, m) end -fun v_elem_at v i = Inttab.curried_lookup v i -fun m_elem_at m i = Inttab.curried_lookup m i +fun v_elem_at v i = Inttab.lookup v i +fun m_elem_at m i = Inttab.lookup m i fun v_only_elem v = case Inttab.min_key v of diff -r 664434175578 -r e26cb20ef0cc src/HOL/Matrix/cplex/fspmlp.ML --- a/src/HOL/Matrix/cplex/fspmlp.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Matrix/cplex/fspmlp.ML Thu Sep 15 17:16:56 2005 +0200 @@ -53,21 +53,21 @@ fun add_row_bound g dest_key row_index row_bound = let val x = - case VarGraph.lookup (g, dest_key) of - NONE => (NONE, Inttab.curried_update (row_index, (row_bound, [])) Inttab.empty) + case VarGraph.lookup g dest_key of + NONE => (NONE, Inttab.update (row_index, (row_bound, [])) Inttab.empty) | SOME (sure_bound, f) => (sure_bound, - case Inttab.curried_lookup f row_index of - NONE => Inttab.curried_update (row_index, (row_bound, [])) f + case Inttab.lookup f row_index of + NONE => Inttab.update (row_index, (row_bound, [])) f | SOME _ => raise (Internal "add_row_bound")) in - VarGraph.update ((dest_key, x), g) + VarGraph.update (dest_key, x) g end fun update_sure_bound g (key as (_, btype)) bound = let val x = - case VarGraph.lookup (g, key) of + case VarGraph.lookup g key of NONE => (SOME bound, Inttab.empty) | SOME (NONE, f) => (SOME bound, f) | SOME (SOME old_bound, f) => @@ -76,30 +76,30 @@ | LOWER => FloatArith.max) old_bound bound), f) in - VarGraph.update ((key, x), g) + VarGraph.update (key, x) g end fun get_sure_bound g key = - case VarGraph.lookup (g, key) of + case VarGraph.lookup g key of NONE => NONE | SOME (sure_bound, _) => sure_bound (*fun get_row_bound g key row_index = - case VarGraph.lookup (g, key) of + case VarGraph.lookup g key of NONE => NONE | SOME (sure_bound, f) => - (case Inttab.curried_lookup f row_index of + (case Inttab.lookup f row_index of NONE => NONE | SOME (row_bound, _) => (sure_bound, row_bound))*) fun add_edge g src_key dest_key row_index coeff = - case VarGraph.lookup (g, dest_key) of + case VarGraph.lookup g dest_key of NONE => raise (Internal "add_edge: dest_key not found") | SOME (sure_bound, f) => - (case Inttab.curried_lookup f row_index of + (case Inttab.lookup f row_index of NONE => raise (Internal "add_edge: row_index not found") | SOME (row_bound, sources) => - VarGraph.curried_update (dest_key, (sure_bound, Inttab.curried_update (row_index, (row_bound, (coeff, src_key) :: sources)) f)) g) + VarGraph.update (dest_key, (sure_bound, Inttab.update (row_index, (row_bound, (coeff, src_key) :: sources)) f)) g) fun split_graph g = let @@ -108,8 +108,8 @@ NONE => (r1, r2) | SOME bound => (case key of - (u, UPPER) => (r1, Inttab.curried_update (u, bound) r2) - | (u, LOWER) => (Inttab.curried_update (u, bound) r1, r2)) + (u, UPPER) => (r1, Inttab.update (u, bound) r2) + | (u, LOWER) => (Inttab.update (u, bound) r1, r2)) in VarGraph.foldl split ((Inttab.empty, Inttab.empty), g) end @@ -163,7 +163,7 @@ | LOWER => FloatArith.max old_bound new_bound)) end in - case VarGraph.lookup (g, key) of + case VarGraph.lookup g key of NONE => NONE | SOME (sure_bound, f) => let @@ -195,7 +195,7 @@ let val empty = Inttab.empty - fun instab t i x = Inttab.curried_update (i, x) t + fun instab t i x = Inttab.update (i, x) t fun isnegstr x = String.isPrefix "-" x fun negstr x = if isnegstr x then String.extract (x, 1, NONE) else "-"^x @@ -280,8 +280,8 @@ let val index = xlen-i val (r, (r12_1, r12_2)) = abs_estimate (i-1) r1 r2 - val b1 = case Inttab.curried_lookup r1 index of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x - val b2 = case Inttab.curried_lookup r2 index of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x + val b1 = case Inttab.lookup r1 index of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x + val b2 = case Inttab.lookup r2 index of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x val abs_max = FloatArith.max (FloatArith.neg (FloatArith.negative_part b1)) (FloatArith.positive_part b2) in (add_row_entry r index abs_max, (add_row_entry r12_1 index b1, add_row_entry r12_2 index b2)) diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Thu Sep 15 17:16:56 2005 +0200 @@ -57,7 +57,7 @@ fun axioms_having_consts_aux [] tab thms = thms | axioms_having_consts_aux (c::cs) tab thms = - let val thms1 = Symtab.curried_lookup tab c + let val thms1 = Symtab.lookup tab c val thms2 = case thms1 of (SOME x) => x | NONE => [] diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Sep 15 17:16:56 2005 +0200 @@ -168,7 +168,7 @@ val inject = map (fn r => r RS iffD1) (if i < length newTs then List.nth (constr_inject, i) - else #inject (the (Symtab.curried_lookup dt_info tname))); + else #inject (the (Symtab.lookup dt_info tname))); fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) = let diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/datatype_aux.ML --- a/src/HOL/Tools/datatype_aux.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/datatype_aux.ML Thu Sep 15 17:16:56 2005 +0200 @@ -299,7 +299,7 @@ Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg); fun get_dt_descr T i tname dts = - (case Symtab.curried_lookup dt_info tname of + (case Symtab.lookup dt_info tname of NONE => typ_error T (tname ^ " is not a datatype - can't use it in\ \ nested recursion") | (SOME {index, descr, ...}) => diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Thu Sep 15 17:16:56 2005 +0200 @@ -281,7 +281,7 @@ | _ => NONE); fun datatype_tycodegen thy defs gr dep module brack (Type (s, Ts)) = - (case Symtab.curried_lookup (DatatypePackage.get_datatypes thy) s of + (case Symtab.lookup (DatatypePackage.get_datatypes thy) s of NONE => NONE | SOME {descr, ...} => if isSome (get_assoc_type thy s) then NONE else diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/datatype_package.ML Thu Sep 15 17:16:56 2005 +0200 @@ -104,7 +104,7 @@ (** theory information about datatypes **) -val datatype_info = Symtab.curried_lookup o get_datatypes; +val datatype_info = Symtab.lookup o get_datatypes; fun datatype_info_err thy name = (case datatype_info thy name of SOME info => info @@ -681,7 +681,7 @@ Theory.add_path (space_implode "_" new_type_names) |> add_rules simps case_thms size_thms rec_thms inject distinct weak_case_congs Simplifier.cong_add_global |> - put_datatypes (fold Symtab.curried_update dt_infos dt_info) |> + put_datatypes (fold Symtab.update dt_infos dt_info) |> add_cases_induct dt_infos induct |> Theory.parent_path |> (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |> @@ -739,7 +739,7 @@ Theory.add_path (space_implode "_" new_type_names) |> add_rules simps case_thms size_thms rec_thms inject distinct weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> - put_datatypes (fold Symtab.curried_update dt_infos dt_info) |> + put_datatypes (fold Symtab.update dt_infos dt_info) |> add_cases_induct dt_infos induct |> Theory.parent_path |> (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |> @@ -847,7 +847,7 @@ Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |> add_rules simps case_thms size_thms rec_thms inject distinct weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> - put_datatypes (fold Symtab.curried_update dt_infos dt_info) |> + put_datatypes (fold Symtab.update dt_infos dt_info) |> add_cases_induct dt_infos induction' |> Theory.parent_path |> (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |> diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Sep 15 17:16:56 2005 +0200 @@ -35,7 +35,7 @@ fun exh_thm_of (dt_info : datatype_info Symtab.table) tname = - #exhaustion (the (Symtab.curried_lookup dt_info tname)); + #exhaustion (the (Symtab.lookup dt_info tname)); (******************************************************************************) @@ -356,7 +356,7 @@ let val ks = map fst ds; val (_, (tname, _, _)) = hd ds; - val {rec_rewrites, rec_names, ...} = the (Symtab.curried_lookup dt_info tname); + val {rec_rewrites, rec_names, ...} = the (Symtab.lookup dt_info tname); fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) = let @@ -412,7 +412,7 @@ fun prove_iso_thms (ds, (inj_thms, elem_thms)) = let val (_, (tname, _, _)) = hd ds; - val {induction, ...} = the (Symtab.curried_lookup dt_info tname); + val {induction, ...} = the (Symtab.lookup dt_info tname); fun mk_ind_concl (i, _) = let diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Thu Sep 15 17:16:56 2005 +0200 @@ -56,7 +56,7 @@ let val cs = foldr add_term_consts [] (prems_of thm) in (CodegenData.put {intros = intros |> - Symtab.curried_update (s, Symtab.curried_lookup_multi intros s @ [(thm, thyname_of s)]), + Symtab.update (s, Symtab.lookup_multi intros s @ [(thm, thyname_of s)]), graph = foldr (uncurry (Graph.add_edge o pair s)) (Library.foldl add_node (graph, s :: cs)) cs, eqns = eqns} thy, thm) @@ -65,15 +65,15 @@ | _ $ (Const ("op =", _) $ t $ _) => (case head_of t of Const (s, _) => (CodegenData.put {intros = intros, graph = graph, - eqns = eqns |> Symtab.curried_update - (s, Symtab.curried_lookup_multi eqns s @ [(thm, thyname_of s)])} thy, thm) + eqns = eqns |> Symtab.update + (s, Symtab.lookup_multi eqns s @ [(thm, thyname_of s)])} thy, thm) | _ => (warn thm; p)) | _ => (warn thm; p)) end; fun get_clauses thy s = let val {intros, graph, ...} = CodegenData.get thy - in case Symtab.curried_lookup intros s of + in case Symtab.lookup intros s of NONE => (case InductivePackage.get_inductive thy s of NONE => NONE | SOME ({names, ...}, {intrs, ...}) => @@ -84,7 +84,7 @@ val SOME names = find_first (fn xs => s mem xs) (Graph.strong_conn graph); val intrs = List.concat (map - (fn s => the (Symtab.curried_lookup intros s)) names); + (fn s => the (Symtab.lookup intros s)) names); val (_, (_, thyname)) = split_last intrs in SOME (names, thyname, preprocess thy (map fst intrs)) end end; @@ -716,7 +716,7 @@ (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"]))) handle TERM _ => mk_ind_call thy defs gr dep module t u true) | inductive_codegen thy defs gr dep module brack t = (case strip_comb t of - (Const (s, _), ts) => (case Symtab.curried_lookup (#eqns (CodegenData.get thy)) s of + (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of NONE => list_of_indset thy defs gr dep module brack t | SOME eqns => let diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/inductive_package.ML Thu Sep 15 17:16:56 2005 +0200 @@ -112,7 +112,7 @@ (* get and put data *) -val get_inductive = Symtab.curried_lookup o #1 o InductiveData.get; +val get_inductive = Symtab.lookup o #1 o InductiveData.get; fun the_inductive thy name = (case get_inductive thy name of @@ -123,7 +123,7 @@ fun put_inductives names info thy = let - fun upd ((tab, monos), name) = (Symtab.curried_update_new (name, info) tab, monos); + fun upd ((tab, monos), name) = (Symtab.update_new (name, info) tab, monos); val tab_monos = Library.foldl upd (InductiveData.get thy, names) handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name); in InductiveData.put tab_monos thy end; diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/primrec_package.ML Thu Sep 15 17:16:56 2005 +0200 @@ -203,7 +203,7 @@ fun find_dts (dt_info : datatype_info Symtab.table) _ [] = [] | find_dts dt_info tnames' (tname::tnames) = - (case Symtab.curried_lookup dt_info tname of + (case Symtab.lookup dt_info tname of NONE => primrec_err (quote tname ^ " is not a datatype") | SOME dt => if tnames' subset (map (#1 o snd) (#descr dt)) then diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/recdef_package.ML Thu Sep 15 17:16:56 2005 +0200 @@ -126,12 +126,12 @@ val print_recdefs = GlobalRecdefData.print; -val get_recdef = Symtab.curried_lookup o #1 o GlobalRecdefData.get; +val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get; fun put_recdef name info thy = let val (tab, hints) = GlobalRecdefData.get thy; - val tab' = Symtab.curried_update_new (name, info) tab + val tab' = Symtab.update_new (name, info) tab handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name); in GlobalRecdefData.put (tab', hints) thy end; diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Thu Sep 15 17:16:56 2005 +0200 @@ -42,7 +42,7 @@ val (s, _) = const_of (prop_of thm); in if Pattern.pattern (lhs_of thm) then - (CodegenData.put (Symtab.curried_update_multi (s, (thm, optmod)) tab) thy, thm) + (CodegenData.put (Symtab.update_multi (s, (thm, optmod)) tab) thy, thm) else (warn thm; p) end handle TERM _ => (warn thm; p); @@ -50,9 +50,9 @@ let val tab = CodegenData.get thy; val (s, _) = const_of (prop_of thm); - in case Symtab.curried_lookup tab s of + in case Symtab.lookup tab s of NONE => p - | SOME thms => (CodegenData.put (Symtab.curried_update (s, + | SOME thms => (CodegenData.put (Symtab.update (s, gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy, thm) end handle TERM _ => (warn thm; p); @@ -64,7 +64,7 @@ in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end; fun get_equations thy defs (s, T) = - (case Symtab.curried_lookup (CodegenData.get thy) s of + (case Symtab.lookup (CodegenData.get thy) s of NONE => ([], "") | SOME thms => let val thms' = del_redundant thy [] diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/record_package.ML Thu Sep 15 17:16:56 2005 +0200 @@ -301,13 +301,13 @@ (* access 'records' *) -val get_record = Symtab.curried_lookup o #records o RecordsData.get; +val get_record = Symtab.lookup o #records o RecordsData.get; fun put_record name info thy = let val {records, sel_upd, equalities, extinjects,extsplit,splits,extfields,fieldext} = RecordsData.get thy; - val data = make_record_data (Symtab.curried_update (name, info) records) + val data = make_record_data (Symtab.update (name, info) records) sel_upd equalities extinjects extsplit splits extfields fieldext; in RecordsData.put data thy end; @@ -315,10 +315,10 @@ val get_sel_upd = #sel_upd o RecordsData.get; -val get_selectors = Symtab.curried_lookup o #selectors o get_sel_upd; +val get_selectors = Symtab.lookup o #selectors o get_sel_upd; fun is_selector sg name = is_some (get_selectors sg (Sign.intern_const sg name)); -val get_updates = Symtab.curried_lookup o #updates o get_sel_upd; +val get_updates = Symtab.lookup o #updates o get_sel_upd; val get_simpset = #simpset o get_sel_upd; fun put_sel_upd names simps thy = @@ -342,11 +342,11 @@ val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy; val data = make_record_data records sel_upd - (Symtab.curried_update_new (name, thm) equalities) extinjects extsplit + (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext; in RecordsData.put data thy end; -val get_equalities =Symtab.curried_lookup o #equalities o RecordsData.get; +val get_equalities =Symtab.lookup o #equalities o RecordsData.get; (* access 'extinjects' *) @@ -367,11 +367,11 @@ val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy; val data = make_record_data records sel_upd - equalities extinjects (Symtab.curried_update_new (name, thm) extsplit) splits + equalities extinjects (Symtab.update_new (name, thm) extsplit) splits extfields fieldext; in RecordsData.put data thy end; -val get_extsplit = Symtab.curried_lookup o #extsplit o RecordsData.get; +val get_extsplit = Symtab.lookup o #extsplit o RecordsData.get; (* access 'splits' *) @@ -380,17 +380,17 @@ val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy; val data = make_record_data records sel_upd - equalities extinjects extsplit (Symtab.curried_update_new (name, thmP) splits) + equalities extinjects extsplit (Symtab.update_new (name, thmP) splits) extfields fieldext; in RecordsData.put data thy end; -val get_splits = Symtab.curried_lookup o #splits o RecordsData.get; +val get_splits = Symtab.lookup o #splits o RecordsData.get; (* extension of a record name *) val get_extension = - Option.map #extension oo (Symtab.curried_lookup o #records o RecordsData.get); + Option.map #extension oo (Symtab.lookup o #records o RecordsData.get); (* access 'extfields' *) @@ -401,10 +401,10 @@ RecordsData.get thy; val data = make_record_data records sel_upd equalities extinjects extsplit splits - (Symtab.curried_update_new (name, fields) extfields) fieldext; + (Symtab.update_new (name, fields) extfields) fieldext; in RecordsData.put data thy end; -val get_extfields = Symtab.curried_lookup o #extfields o RecordsData.get; +val get_extfields = Symtab.lookup o #extfields o RecordsData.get; fun get_extT_fields sg T = let @@ -415,8 +415,8 @@ fun varify (a, S) = TVar ((a, midx), S); val varifyT = map_type_tfree varify; val {records,extfields,...} = RecordsData.get sg; - val (flds,(more,_)) = split_last (Symtab.curried_lookup_multi extfields name); - val args = map varifyT (snd (#extension (the (Symtab.curried_lookup records recname)))); + val (flds,(more,_)) = split_last (Symtab.lookup_multi extfields name); + val args = map varifyT (snd (#extension (the (Symtab.lookup records recname)))); val (subst,_) = fold (Sign.typ_unify sg) (but_last args ~~ but_last Ts) (Vartab.empty,0); val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds; @@ -438,13 +438,13 @@ val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = RecordsData.get thy; val fieldext' = - fold (fn field => Symtab.curried_update_new (field, extname_types)) fields fieldext; + fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext; val data=make_record_data records sel_upd equalities extinjects extsplit splits extfields fieldext'; in RecordsData.put data thy end; -val get_fieldext = Symtab.curried_lookup o #fieldext o RecordsData.get; +val get_fieldext = Symtab.lookup o #fieldext o RecordsData.get; (* parent records *) @@ -819,7 +819,7 @@ let val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg; val extsplits = - Library.foldl (fn (thms,(n,_)) => the_list (Symtab.curried_lookup extsplit n) @ thms) + Library.foldl (fn (thms,(n,_)) => the_list (Symtab.lookup extsplit n) @ thms) ([],dest_recTs T); val thms = (case get_splits sg (rec_id (~1) T) of SOME (all_thm,_,_,_) => @@ -835,7 +835,7 @@ local fun eq (s1:string) (s2:string) = (s1 = s2); fun has_field extfields f T = - exists (fn (eN,_) => exists (eq f o fst) (Symtab.curried_lookup_multi extfields eN)) + exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_multi extfields eN)) (dest_recTs T); in (* record_simproc *) @@ -861,7 +861,7 @@ val {sel_upd={updates,...},extfields,...} = RecordsData.get sg; fun mk_eq_terms ((upd as Const (u,Type(_,[kT,_]))) $ k $ r) = - (case Symtab.curried_lookup updates u of + (case Symtab.lookup updates u of NONE => NONE | SOME u_name => if u_name = s diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/refute.ML Thu Sep 15 17:16:56 2005 +0200 @@ -298,11 +298,11 @@ let val {interpreters, printers, parameters} = RefuteData.get thy in - case Symtab.curried_lookup parameters name of + case Symtab.lookup parameters name of NONE => RefuteData.put {interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy | SOME _ => RefuteData.put - {interpreters = interpreters, printers = printers, parameters = Symtab.curried_update (name, value) parameters} thy + {interpreters = interpreters, printers = printers, parameters = Symtab.update (name, value) parameters} thy end; (* ------------------------------------------------------------------------- *) @@ -312,7 +312,7 @@ (* theory -> string -> string option *) - val get_default_param = Symtab.curried_lookup o #parameters o RefuteData.get; + val get_default_param = Symtab.lookup o #parameters o RefuteData.get; (* ------------------------------------------------------------------------- *) (* get_default_params: returns a list of all '(name, value)' pairs that are *) diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Sep 15 17:16:56 2005 +0200 @@ -261,7 +261,7 @@ (*Populate the clause cache using the supplied theorems*) fun skolemlist [] thy = thy | skolemlist ((name,th)::nths) thy = - (case Symtab.curried_lookup (!clause_cache) name of + (case Symtab.lookup (!clause_cache) name of NONE => let val (nnfth,ok) = (to_nnf thy th, true) handle THM _ => (asm_rl, false) @@ -269,7 +269,7 @@ if ok then let val (skoths,thy') = skolem thy (name, nnfth) val cls = Meson.make_cnf skoths nnfth - in change clause_cache (Symtab.curried_update (name, (th, cls))); + in change clause_cache (Symtab.update (name, (th, cls))); skolemlist nths thy' end else skolemlist nths thy @@ -280,15 +280,15 @@ fun cnf_axiom (name,th) = case name of "" => cnf_axiom_aux th (*no name, so can't cache*) - | s => case Symtab.curried_lookup (!clause_cache) s of + | s => case Symtab.lookup (!clause_cache) s of NONE => let val cls = cnf_axiom_aux th - in change clause_cache (Symtab.curried_update (s, (th, cls))); cls end + in change clause_cache (Symtab.update (s, (th, cls))); cls end | SOME(th',cls) => if eq_thm(th,th') then cls else (*New theorem stored under the same name? Possible??*) let val cls = cnf_axiom_aux th - in change clause_cache (Symtab.curried_update (s, (th, cls))); cls end; + in change clause_cache (Symtab.update (s, (th, cls))); cls end; fun pairname th = (Thm.name_of_thm th, th); diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Thu Sep 15 17:16:56 2005 +0200 @@ -141,12 +141,12 @@ fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); fun make_fixed_const c = - case Symtab.curried_lookup const_trans_table c of + case Symtab.lookup const_trans_table c of SOME c' => c' | NONE => const_prefix ^ ascii_of c; fun make_fixed_type_const c = - case Symtab.curried_lookup type_const_trans_table c of + case Symtab.lookup type_const_trans_table c of SOME c' => c' | NONE => tconst_prefix ^ ascii_of c; diff -r 664434175578 -r e26cb20ef0cc src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/HOL/Tools/typedef_package.ML Thu Sep 15 17:16:56 2005 +0200 @@ -62,7 +62,7 @@ end); fun put_typedef newT oldT Abs_name Rep_name = - TypedefData.map (Symtab.curried_update_new (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name))); + TypedefData.map (Symtab.update_new (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name))); @@ -299,7 +299,7 @@ val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'') in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end; fun lookup f T = - (case Symtab.curried_lookup (TypedefData.get thy) (get_name T) of + (case Symtab.lookup (TypedefData.get thy) (get_name T) of NONE => "" | SOME s => f s); in @@ -320,7 +320,7 @@ | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) = - (case Symtab.curried_lookup (TypedefData.get thy) s of + (case Symtab.lookup (TypedefData.get thy) s of NONE => NONE | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) => if is_some (Codegen.get_assoc_type thy tname) then NONE else diff -r 664434175578 -r e26cb20ef0cc src/Provers/Arith/cancel_numerals.ML --- a/src/Provers/Arith/cancel_numerals.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Provers/Arith/cancel_numerals.ML Thu Sep 15 17:16:56 2005 +0200 @@ -54,7 +54,7 @@ (*For t = #n*u then put u in the table*) fun update_by_coeff t = - Termtab.curried_update (#2 (Data.dest_coeff t), ()); + Termtab.update (#2 (Data.dest_coeff t), ()); (*a left-to-right scan of terms1, seeking a term of the form #n*u, where #m*u is in terms2 for some m*) diff -r 664434175578 -r e26cb20ef0cc src/Provers/Arith/combine_numerals.ML --- a/src/Provers/Arith/combine_numerals.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Provers/Arith/combine_numerals.ML Thu Sep 15 17:16:56 2005 +0200 @@ -57,9 +57,9 @@ | find_repeated (tab, past, t::terms) = case try Data.dest_coeff t of SOME(n,u) => - (case Termtab.curried_lookup tab u of + (case Termtab.lookup tab u of SOME m => (u, m, n, rev (remove (m,u,past)) @ terms) - | NONE => find_repeated (Termtab.curried_update (u, n) tab, + | NONE => find_repeated (Termtab.update (u, n) tab, t::past, terms)) | NONE => find_repeated (tab, t::past, terms); diff -r 664434175578 -r e26cb20ef0cc src/Provers/Arith/extract_common_term.ML --- a/src/Provers/Arith/extract_common_term.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Provers/Arith/extract_common_term.ML Thu Sep 15 17:16:56 2005 +0200 @@ -39,7 +39,7 @@ (*a left-to-right scan of terms1, seeking a term u that is also in terms2*) fun find_common (terms1,terms2) = - let val tab2 = fold (Termtab.curried_update o rpair ()) terms2 Termtab.empty + let val tab2 = fold (Termtab.update o rpair ()) terms2 Termtab.empty fun seek [] = raise TERM("find_common", []) | seek (u::terms) = if Termtab.defined tab2 u then u diff -r 664434175578 -r e26cb20ef0cc src/Pure/General/graph.ML --- a/src/Pure/General/graph.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/General/graph.ML Thu Sep 15 17:16:56 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.curried_lookup tab x of + (case Table.lookup tab x of SOME entry => entry | NONE => raise UNDEF x); -fun map_entry x f (G as Graph tab) = Graph (Table.curried_update (x, f (get_entry G x)) tab); +fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab); (* nodes *) @@ -142,7 +142,7 @@ (* nodes *) fun new_node (x, info) (Graph tab) = - Graph (Table.curried_update_new (x, (info, ([], []))) tab); + Graph (Table.update_new (x, (info, ([], []))) tab); fun default_node (x, info) (Graph tab) = Graph (Table.default (x, (info, ([], []))) tab); diff -r 664434175578 -r e26cb20ef0cc src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/General/name_space.ML Thu Sep 15 17:16:56 2005 +0200 @@ -113,7 +113,7 @@ val empty = NameSpace Symtab.empty; fun lookup (NameSpace tab) xname = - (case Symtab.curried_lookup tab xname of + (case Symtab.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.curried_update (xname, f (if_none (Symtab.curried_lookup tab xname) ([], []))) tab); + NameSpace (Symtab.update (xname, f (if_none (Symtab.lookup tab xname) ([], []))) tab); fun del (name: string) = remove (op =) name; fun add name names = name :: del name names; diff -r 664434175578 -r e26cb20ef0cc src/Pure/General/output.ML --- a/src/Pure/General/output.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/General/output.ML Thu Sep 15 17:16:56 2005 +0200 @@ -84,7 +84,7 @@ exception MISSING_DEFAULT_OUTPUT; -fun lookup_mode name = Symtab.curried_lookup (! modes) name; +fun lookup_mode name = Symtab.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.curried_update (name, {output_width = f, indent = g, raw = h}) (! modes)); + modes := Symtab.update (name, {output_width = f, indent = g, raw = h}) (! modes)); (* produce errors *) diff -r 664434175578 -r e26cb20ef0cc src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/General/symbol.ML Thu Sep 15 17:16:56 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.curried_lookup symbol_kinds s) Other; + else if_none (Symtab.lookup symbol_kinds s) Other; end; fun is_letter s = kind s = Letter; diff -r 664434175578 -r e26cb20ef0cc src/Pure/General/table.ML --- a/src/Pure/General/table.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/General/table.ML Thu Sep 15 17:16:56 2005 +0200 @@ -32,12 +32,9 @@ val exists: (key * 'a -> bool) -> 'a table -> bool val forall: (key * 'a -> bool) -> 'a table -> bool val defined: 'a table -> key -> bool - val lookup: 'a table * key -> 'a option - val update: (key * 'a) * 'a table -> 'a table - val update_new: (key * 'a) * 'a table -> 'a table (*exception DUP*) - val curried_lookup: 'a table -> key -> 'a option - val curried_update: (key * 'a) -> 'a table -> 'a table - val curried_update_new: (key * 'a) -> 'a table -> 'a table (*exception DUP*) + val lookup: 'a table -> key -> 'a option + val update: (key * 'a) -> 'a table -> 'a table + val update_new: (key * 'a) -> 'a table -> 'a table (*exception DUP*) val default: key * 'a -> 'a table -> 'a table val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table val make: (key * 'a) list -> 'a table (*exception DUPS*) @@ -50,10 +47,8 @@ val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table (*exception DUP*) val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table - val lookup_multi: 'a list table * key -> 'a list - val update_multi: (key * 'a) * 'a list table -> 'a list table - val curried_lookup_multi: 'a list table -> key -> 'a list - val curried_update_multi: (key * 'a) -> 'a list table -> 'a list table + val lookup_multi: 'a list table -> key -> 'a list + val update_multi: (key * 'a) -> 'a list table -> 'a list table val remove_multi: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table val make_multi: (key * 'a) list -> 'a list table val dest_multi: 'a list table -> (key * 'a) list @@ -136,25 +131,23 @@ (* lookup *) -fun curried_lookup Empty _ = NONE - | curried_lookup (Branch2 (left, (k, x), right)) key = +fun lookup Empty _ = NONE + | lookup (Branch2 (left, (k, x), right)) key = (case Key.ord (key, k) of - LESS => curried_lookup left key + LESS => lookup left key | EQUAL => SOME x - | GREATER => curried_lookup right key) - | curried_lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right)) key = + | GREATER => lookup right key) + | lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right)) key = (case Key.ord (key, k1) of - LESS => curried_lookup left key + LESS => lookup left key | EQUAL => SOME x1 | GREATER => (case Key.ord (key, k2) of - LESS => curried_lookup mid key + LESS => lookup mid key | EQUAL => SOME x2 - | GREATER => curried_lookup right key)); + | GREATER => lookup right key)); -fun lookup (tab, key) = curried_lookup tab key; - -fun defined tab key = is_some (curried_lookup tab key); +fun defined tab key = is_some (lookup tab key); (* updates *) @@ -209,11 +202,9 @@ handle SAME => tab end; -fun update ((key, x), tab) = modify key (fn _ => x) tab; -fun update_new ((key, x), tab) = modify key (fn NONE => x | SOME _ => raise DUP key) tab; -fun curried_update (key, x) tab = modify key (fn _ => x) tab; -fun curried_update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab; -fun default (p as (key, x)) tab = if defined tab key then tab else curried_update p tab; +fun update (key, x) tab = modify key (fn _ => x) tab; +fun update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab; +fun default (p as (key, x)) tab = if defined tab key then tab else update p tab; fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x); @@ -223,7 +214,7 @@ let fun add (key, x) (tab, dups) = if defined tab key then (tab, key :: dups) - else (curried_update (key, x) tab, dups); + else (update (key, x) tab, dups); in (case fold add args (table, []) of (table', []) => table' @@ -319,7 +310,7 @@ (* member, insert and remove *) fun member eq tab (key, x) = - (case curried_lookup tab key of + (case lookup tab key of NONE => false | SOME y => eq (x, y)); @@ -327,7 +318,7 @@ modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else raise DUP key); fun remove eq (key, x) tab = - (case curried_lookup tab key of + (case lookup tab key of NONE => tab | SOME y => if eq (x, y) then delete key tab else tab); @@ -337,11 +328,11 @@ fun join f (table1, table2) = let fun add (key, x) (tab, dups) = - (case curried_lookup tab key of - NONE => (curried_update (key, x) tab, dups) + (case lookup tab key of + NONE => (update (key, x) tab, dups) | SOME y => (case f key (y, x) of - SOME z => (curried_update (key, z) tab, dups) + SOME z => (update (key, z) tab, dups) | NONE => (tab, key :: dups))); in (case fold_table add table2 (table1, []) of @@ -354,17 +345,14 @@ (* tables with multiple entries per key *) -fun lookup_multi arg = if_none (lookup arg) []; -fun update_multi ((key, x), tab) = modify key (fn NONE => [x] | SOME xs => x :: xs) tab; - -fun curried_lookup_multi tab key = if_none (curried_lookup tab key) []; -fun curried_update_multi (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab; +fun lookup_multi tab key = if_none (lookup tab key) []; +fun update_multi (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab; fun remove_multi eq (key, x) tab = map_entry key (fn xs => (case Library.remove eq x xs of [] => raise UNDEF key | ys => ys)) tab handle UNDEF _ => delete key tab; -fun make_multi args = fold_rev curried_update_multi args empty; +fun make_multi args = fold_rev update_multi args empty; fun dest_multi tab = List.concat (map (fn (key, xs) => map (pair key) xs) (dest tab)); fun merge_multi eq = join (fn _ => fn (xs, xs') => SOME (gen_merge_lists eq xs xs')); fun merge_multi' eq = join (fn _ => fn (xs, xs') => SOME (gen_merge_lists' eq xs xs')); diff -r 664434175578 -r e26cb20ef0cc src/Pure/IsaPlanner/term_lib.ML --- a/src/Pure/IsaPlanner/term_lib.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/IsaPlanner/term_lib.ML Thu Sep 15 17:16:56 2005 +0200 @@ -516,10 +516,10 @@ (* a runtime-quick function which makes sure that every variable has a unique name *) fun unique_namify_aux (ntab,(Abs(s,ty,t))) = - (case Symtab.curried_lookup ntab s of + (case Symtab.lookup ntab s of NONE => let - val (ntab2,t2) = unique_namify_aux (Symtab.curried_update (s, s) ntab, t) + val (ntab2,t2) = unique_namify_aux (Symtab.update (s, s) ntab, t) in (ntab2,Abs(s,ty,t2)) end @@ -527,7 +527,7 @@ let val s_new = (Term.variant (Symtab.keys ntab) s) val (ntab2,t2) = - unique_namify_aux (Symtab.curried_update (s_new, s_new) ntab, t) + unique_namify_aux (Symtab.update (s_new, s_new) ntab, t) in (ntab2,Abs(s_new,ty,t2)) end) @@ -540,12 +540,12 @@ end | unique_namify_aux (nt as (ntab,Const x)) = nt | unique_namify_aux (nt as (ntab,f as Free (s,ty))) = - (case Symtab.curried_lookup ntab s of - NONE => (Symtab.curried_update (s, s) ntab, f) + (case Symtab.lookup ntab s of + NONE => (Symtab.update (s, s) ntab, f) | SOME _ => nt) | unique_namify_aux (nt as (ntab,v as Var ((s,i),ty))) = - (case Symtab.curried_lookup ntab s of - NONE => (Symtab.curried_update (s, s) ntab, v) + (case Symtab.lookup ntab s of + NONE => (Symtab.update (s, s) ntab, v) | SOME _ => nt) | unique_namify_aux (nt as (ntab, Bound i)) = nt; @@ -559,11 +559,11 @@ sematics of the term. This is really a trick for our embedding code. *) fun bounds_to_frees_aux T (ntab,(Abs(s,ty,t))) = - (case Symtab.curried_lookup ntab s of + (case Symtab.lookup ntab s of NONE => let val (ntab2,t2) = - bounds_to_frees_aux ((s,ty)::T) (Symtab.curried_update (s, s) ntab, t) + bounds_to_frees_aux ((s,ty)::T) (Symtab.update (s, s) ntab, t) in (ntab2,Abs(s,ty,t2)) end @@ -572,7 +572,7 @@ val s_new = (Term.variant (Symtab.keys ntab) s) val (ntab2,t2) = bounds_to_frees_aux ((s_new,ty)::T) - (Symtab.curried_update (s_new, s_new) ntab, t) + (Symtab.update (s_new, s_new) ntab, t) in (ntab2,Abs(s_new,ty,t2)) end) @@ -585,12 +585,12 @@ end | bounds_to_frees_aux T (nt as (ntab,Const x)) = nt | bounds_to_frees_aux T (nt as (ntab,f as Free (s,ty))) = - (case Symtab.curried_lookup ntab s of - NONE => (Symtab.curried_update (s, s) ntab, f) + (case Symtab.lookup ntab s of + NONE => (Symtab.update (s, s) ntab, f) | SOME _ => nt) | bounds_to_frees_aux T (nt as (ntab,v as Var ((s,i),ty))) = - (case Symtab.curried_lookup ntab s of - NONE => (Symtab.curried_update (s, s) ntab, v) + (case Symtab.lookup ntab s of + NONE => (Symtab.update (s, s) ntab, v) | SOME _ => nt) | bounds_to_frees_aux T (nt as (ntab, Bound i)) = let diff -r 664434175578 -r e26cb20ef0cc src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Isar/attrib.ML Thu Sep 15 17:16:56 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.curried_lookup attrs name of + (case Symtab.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 664434175578 -r e26cb20ef0cc src/Pure/Isar/isar_output.ML --- a/src/Pure/Isar/isar_output.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Isar/isar_output.ML Thu Sep 15 17:16:56 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.curried_update (name, x) tab); + Symtab.update (name, x) tab); in @@ -68,13 +68,13 @@ fun command src = let val ((name, _), pos) = Args.dest_src src in - (case Symtab.curried_lookup (! global_commands) name of + (case Symtab.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.curried_lookup (! global_options) name of + (case Symtab.lookup (! global_options) name of NONE => error ("Unknown antiquotation option: " ^ quote name) | SOME opt => opt s f ()); diff -r 664434175578 -r e26cb20ef0cc src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Isar/locale.ML Thu Sep 15 17:16:56 2005 +0200 @@ -182,7 +182,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.curried_lookup tinst x, (TFree v))) T; + (fn (v as (x, _)) => getOpt (Symtab.lookup tinst x, (TFree v))) T; fun tinst_tab_term tinst t = if Symtab.is_empty tinst then t @@ -215,7 +215,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.curried_lookup inst x of + | instf (Free (x, T)) = (case Symtab.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) @@ -336,7 +336,7 @@ val sups = List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs); val sups' = map (apfst untermify) sups - in (Termtab.curried_update (t, (attn, [])) regs, sups') end + in (Termtab.update (t, (attn, [])) regs, sups') end | _ => (regs, [])) end; @@ -345,9 +345,9 @@ fun add_witness ts thm regs = let val t = termify ts; - val (x, thms) = valOf (Termtab.curried_lookup regs t); + val (x, thms) = valOf (Termtab.lookup regs t); in - Termtab.curried_update (t, (x, thm::thms)) regs + Termtab.update (t, (x, thm::thms)) regs end; end; @@ -412,9 +412,9 @@ fun put_locale name loc = GlobalLocalesData.map (fn (space, locs, regs) => - (space, Symtab.curried_update (name, loc) locs, regs)); - -fun get_locale thy name = Symtab.curried_lookup (#2 (GlobalLocalesData.get thy)) name; + (space, Symtab.update (name, loc) locs, regs)); + +fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name; fun the_locale thy name = (case get_locale thy name of @@ -431,7 +431,7 @@ (* retrieve registration from theory or context *) fun gen_get_registrations get thy_ctxt name = - case Symtab.curried_lookup (get thy_ctxt) name of + case Symtab.lookup (get thy_ctxt) name of NONE => [] | SOME reg => Registrations.dest reg; @@ -441,7 +441,7 @@ gen_get_registrations LocalLocalesData.get; fun gen_get_registration get thy_of thy_ctxt (name, ps) = - case Symtab.curried_lookup (get thy_ctxt) name of + case Symtab.lookup (get thy_ctxt) name of NONE => NONE | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps); @@ -466,7 +466,7 @@ map_data (fn regs => let val thy = thy_of thy_ctxt; - val reg = getOpt (Symtab.curried_lookup regs name, Registrations.empty); + val reg = getOpt (Symtab.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 " ^ @@ -474,7 +474,7 @@ "\nby interpretation(s) with the following prefix(es):\n" ^ commas_quote (map (fn (_, ((s, _), _)) => s) sups)) else (); - in Symtab.curried_update (name, reg') regs end) thy_ctxt; + in Symtab.update (name, reg') regs end) thy_ctxt; val put_global_registration = gen_put_registration (fn f => @@ -559,7 +559,7 @@ val loc_int = intern thy loc; val regs = get_regs thy_ctxt; - val loc_regs = Symtab.curried_lookup regs loc_int; + val loc_regs = Symtab.lookup regs loc_int; in (case loc_regs of NONE => Pretty.str ("no interpretations in " ^ msg) @@ -771,7 +771,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.curried_lookup syn x)))); + map (apfst (fn x => (x, valOf (Symtab.lookup syn x)))); (* CB: param_types has the following type: @@ -1017,7 +1017,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.curried_lookup syn x))) xs; + map (fn x => (x, valOf (Symtab.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), @@ -1754,7 +1754,7 @@ |> Symtab.make; (* replace parameter names in ids by instantiations *) val vinst = Symtab.make (parms ~~ vts); - fun vinst_names ps = map (the o Symtab.curried_lookup vinst) ps; + fun vinst_names ps = map (the o Symtab.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'); @@ -2028,7 +2028,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), the (Symtab.curried_lookup syn x))), map #1 (params_of body_elemss)), + map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), map #1 (params_of body_elemss)), regs = []} |> pair (elems', body_ctxt) end; @@ -2264,7 +2264,7 @@ NONE => error ("Instance missing for parameter " ^ quote p) | SOME (Free (_, T), t) => (t, T); val d = inst_tab_term (inst, tinst) t; - in (Symtab.curried_update_new (p, d) inst, tinst) end; + in (Symtab.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 664434175578 -r e26cb20ef0cc src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Isar/method.ML Thu Sep 15 17:16:56 2005 +0200 @@ -570,7 +570,7 @@ val ((raw_name, _), pos) = Args.dest_src src; val name = NameSpace.intern space raw_name; in - (case Symtab.curried_lookup meths name of + (case Symtab.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 664434175578 -r e26cb20ef0cc src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Thu Sep 15 17:16:56 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 Symtab.curried_lookup (get_parsers ()); +fun get_parser () = Option.map (#2 o #1) o Symtab.lookup (get_parsers ()); fun command_tags name = - (case Symtab.curried_lookup (get_parsers ()) name of + (case Symtab.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.curried_update (name, (((comment, kind), (int_only, parse)), markup)) tab); + Symtab.update (name, (((comment, kind), (int_only, parse)), markup)) tab); fun add_parsers parsers = (change_parsers (fold add_parser parsers); diff -r 664434175578 -r e26cb20ef0cc src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Sep 15 17:16:56 2005 +0200 @@ -365,18 +365,18 @@ (** default sorts and types **) -val def_sort = Vartab.curried_lookup o #2 o defaults_of; +val def_sort = Vartab.lookup o #2 o defaults_of; fun def_type ctxt pattern xi = let val {binds, defs = (types, _, _, _), ...} = rep_context ctxt in - (case Vartab.curried_lookup types xi of + (case Vartab.lookup types xi of NONE => if pattern then NONE - else Vartab.curried_lookup binds xi |> Option.map (TypeInfer.polymorphicT o #2) + else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #2) | some => some) end; -fun default_type ctxt x = Vartab.curried_lookup (#1 (defaults_of ctxt)) (x, ~1); +fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt)) (x, ~1); val used_types = #3 o defaults_of; @@ -493,7 +493,7 @@ val binds = binds_of ctxt; fun norm (t as Var (xi, T)) = - (case Vartab.curried_lookup binds xi of + (case Vartab.lookup binds xi of SOME (u, U) => let val env = unifyT ctxt (T, U) handle Type.TUNIFY => @@ -597,24 +597,24 @@ local val ins_types = fold_aterms - (fn Free (x, T) => Vartab.curried_update ((x, ~1), T) - | Var v => Vartab.curried_update v + (fn Free (x, T) => Vartab.update ((x, ~1), T) + | Var v => Vartab.update v | _ => I); val ins_sorts = fold_types (fold_atyps - (fn TFree (x, S) => Vartab.curried_update ((x, ~1), S) - | TVar v => Vartab.curried_update v + (fn TFree (x, S) => Vartab.update ((x, ~1), S) + | TVar v => Vartab.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, _) => Symtab.curried_update_multi (x, t) | _ => I)); + fold_atyps (fn TFree (x, _) => Symtab.update_multi (x, t) | _ => I)); fun ins_skolem def_ty = fold_rev (fn (x, x') => (case def_ty x' of - SOME T => Vartab.curried_update ((x, ~1), T) + SOME T => Vartab.update ((x, ~1), T) | NONE => I)); fun map_defaults f = map_context (fn (syntax, asms, binds, thms, cases, defs) => @@ -633,7 +633,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.curried_lookup types (x, ~1)) (fixes_of ctxt) types, + (ins_skolem (fn x => Vartab.lookup types (x, ~1)) (fixes_of ctxt) types, sorts, used, occ)); end; @@ -691,7 +691,7 @@ val occs_outer = type_occs_of outer; fun add a gen = if Symtab.defined occs_outer a orelse - exists still_fixed (Symtab.curried_lookup_multi occs_inner a) + exists still_fixed (Symtab.lookup_multi occs_inner a) then gen else a :: gen; in fn tfrees => fold add tfrees [] end; @@ -774,7 +774,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.curried_update ((x, i), (t', T)) binds, thms, cases, defs)) + (syntax, asms, Vartab.update ((x, i), (t', T)) binds, thms, cases, defs)) o declare_term t' end; @@ -932,7 +932,7 @@ val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref; val name = PureThy.name_of_thmref thmref; in - (case Symtab.curried_lookup tab name of + (case Symtab.lookup tab name of SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths) | NONE => from_thy thy xthmref) |> pick name end @@ -993,7 +993,7 @@ let val name = NameSpace.full naming bname; val space' = NameSpace.declare naming name space; - val tab' = Symtab.curried_update (name, ths) tab; + val tab' = Symtab.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 664434175578 -r e26cb20ef0cc src/Pure/Isar/term_style.ML --- a/src/Pure/Isar/term_style.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Isar/term_style.ML Thu Sep 15 17:16:56 2005 +0200 @@ -40,12 +40,12 @@ (* accessors *) fun the_style thy name = - (case Symtab.curried_lookup (StyleData.get thy) name of + (case Symtab.lookup (StyleData.get thy) name of NONE => error ("Unknown antiquote style: " ^ quote name) | SOME (style, _) => style); fun add_style name style thy = - StyleData.map (Symtab.curried_update_new (name, (style, stamp ()))) thy + StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy handle Symtab.DUP _ => err_dup_styles [name]; diff -r 664434175578 -r e26cb20ef0cc src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Proof/extraction.ML Thu Sep 15 17:16:56 2005 +0200 @@ -301,7 +301,7 @@ in ExtractionData.put {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types, - realizers = fold (Symtab.curried_update_multi o prep_rlz thy) rs realizers, + realizers = fold (Symtab.update_multi o prep_rlz thy) rs realizers, defs = defs, expand = expand, prep = prep} thy end @@ -564,7 +564,7 @@ else fst (extr d defs vs ts Ts hs prf0) in if T = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0) - else case Symtab.curried_lookup realizers name of + else case Symtab.lookup realizers name of NONE => (case find vs' (find' name defs') of NONE => let @@ -600,7 +600,7 @@ in if etype_of thy' vs' [] prop = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0) - else case find vs' (Symtab.curried_lookup_multi realizers s) of + else case find vs' (Symtab.lookup_multi realizers s) of SOME (_, prf) => (defs, prf_subst_TVars tye' prf) | NONE => error ("corr: no realizer for instance of axiom " ^ quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm @@ -648,7 +648,7 @@ val (vs', tye) = find_inst prop Ts ts vs; val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye in - case Symtab.curried_lookup realizers s of + case Symtab.lookup realizers s of NONE => (case find vs' (find' s defs) of NONE => let @@ -707,7 +707,7 @@ val (vs', tye) = find_inst prop Ts ts vs; val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye in - case find vs' (Symtab.curried_lookup_multi realizers s) of + case find vs' (Symtab.lookup_multi realizers s) of SOME (t, _) => (defs, subst_TVars tye' t) | NONE => error ("extr: no realizer for instance of axiom " ^ quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm diff -r 664434175578 -r e26cb20ef0cc src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Thu Sep 15 17:16:56 2005 +0200 @@ -100,7 +100,7 @@ let val prop = if_none (AList.lookup (op =) thms' key) (Bound 0) in fst (foldr (fn ((prop', prf), x as (tab, i)) => if prop <> prop' then - (Symtab.curried_update (key ^ "_" ^ string_of_int i, prf) tab, i+1) + (Symtab.update (key ^ "_" ^ string_of_int i, prf) tab, i+1) else x) (tab, 1) ps) end) (Symtab.empty, thms); @@ -111,7 +111,7 @@ | rename (prf' as PThm ((s, tags), prf, prop, Ts)) = let val prop' = if_none (AList.lookup (op =) thms' s) (Bound 0); - val ps = map fst (the (Symtab.curried_lookup thms s)) \ prop' + val ps = map fst (the (Symtab.lookup thms s)) \ prop' in if prop = prop' then prf' else PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags), prf, prop, Ts) @@ -146,7 +146,7 @@ let val name = NameSpace.pack xs; in (case AList.lookup (op =) thms name of SOME thm => fst (strip_combt (Thm.proof_of thm)) - | NONE => (case Symtab.curried_lookup tab name of + | NONE => (case Symtab.lookup tab name of SOME prf => prf | NONE => error ("Unknown theorem " ^ quote name))) end diff -r 664434175578 -r e26cb20ef0cc src/Pure/Proof/proofchecker.ML --- a/src/Pure/Proof/proofchecker.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Proof/proofchecker.ML Thu Sep 15 17:16:56 2005 +0200 @@ -19,9 +19,9 @@ (***** construct a theorem out of a proof term *****) fun lookup_thm thy = - let val tab = fold_rev Symtab.curried_update (PureThy.all_thms_of thy) Symtab.empty + let val tab = fold_rev Symtab.update (PureThy.all_thms_of thy) Symtab.empty in - (fn s => case Symtab.curried_lookup tab s of + (fn s => case Symtab.lookup tab s of NONE => error ("Unknown theorem " ^ quote s) | SOME thm => thm) end; diff -r 664434175578 -r e26cb20ef0cc src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Proof/reconstruct.ML Thu Sep 15 17:16:56 2005 +0200 @@ -81,10 +81,10 @@ end) else (t, T, vTs, env) | infer_type sg env Ts vTs (t as Free (s, T)) = - if T = dummyT then (case Symtab.curried_lookup vTs s of + if T = dummyT then (case Symtab.lookup vTs s of NONE => let val (env', T) = mk_tvar (env, []) - in (Free (s, T), T, Symtab.curried_update_new (s, T) vTs, env') end + in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end | SOME T => (Free (s, T), T, vTs, env)) else (t, T, vTs, env) | infer_type sg env Ts vTs (Var _) = error "reconstruct_proof: internal error" diff -r 664434175578 -r e26cb20ef0cc src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Syntax/ast.ML Thu Sep 15 17:16:56 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.curried_update (x, ast) env + | mtch ast (Variable x) env = Symtab.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.curried_lookup env x) + | subst env (Variable x) = the (Symtab.lookup env x) | subst env (Appl asts) = Appl (map (subst env) asts); fun try_rules ((lhs, rhs) :: pats) ast = diff -r 664434175578 -r e26cb20ef0cc src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Syntax/parser.ML Thu Sep 15 17:16:56 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.curried_lookup tags nt of + case Symtab.lookup tags nt of SOME tag => (nt_count, tags, tag) - | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags, + | NONE => (nt_count+1, Symtab.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.curried_lookup tags nt of + case Symtab.lookup tags nt of SOME tag => (nt_count, tags, tag) - | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags, + | NONE => (nt_count+1, Symtab.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.curried_lookup tags startsymbol of + val start_tag = case Symtab.lookup tags startsymbol of SOME tag => tag | NONE => error ("parse: Unknown startsymbol " ^ quote startsymbol); diff -r 664434175578 -r e26cb20ef0cc src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Syntax/printer.ML Thu Sep 15 17:16:56 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 Symtab.curried_update_multi m; +fun extend_prtabs m = change_prtabs Symtab.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.curried_lookup_multi tb a, tbs) + | prnt ([], tb :: tbs) = prnt (Symtab.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 664434175578 -r e26cb20ef0cc src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Syntax/syntax.ML Thu Sep 15 17:16:56 2005 +0200 @@ -82,7 +82,7 @@ (* parse (ast) translations *) -fun lookup_tr tab c = Option.map fst (Symtab.curried_lookup tab c); +fun lookup_tr tab c = Option.map fst (Symtab.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.curried_lookup_multi tab c); -fun extend_tr'tab trfuns = fold_rev Symtab.curried_update_multi trfuns; +fun lookup_tr' tab c = map fst (Symtab.lookup_multi tab c); +fun extend_tr'tab trfuns = fold_rev Symtab.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); @@ -151,7 +151,7 @@ (* empty, extend, merge ruletabs *) -val extend_ruletab = fold_rev (fn r => Symtab.curried_update_multi (Ast.head_of_rule r, r)); +val extend_ruletab = fold_rev (fn r => Symtab.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); @@ -385,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 (Symtab.curried_lookup_multi parse_ruletab)) asts) + (map (Ast.normalize_ast (Symtab.lookup_multi parse_ruletab)) asts) end; @@ -469,7 +469,7 @@ in prt_t thy curried prtabs (lookup_tr' print_ast_trtab) (lookup_tokentr tokentrtab (! print_mode)) - (Ast.normalize_ast (Symtab.curried_lookup_multi print_ruletab) ast) + (Ast.normalize_ast (Symtab.lookup_multi print_ruletab) ast) end; val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast; diff -r 664434175578 -r e26cb20ef0cc src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Thy/html.ML Thu Sep 15 17:16:56 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.curried_lookup html_syms s of SOME x => x + (case Symtab.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 664434175578 -r e26cb20ef0cc src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Thy/present.ML Thu Sep 15 17:16:56 2005 +0200 @@ -172,13 +172,13 @@ fun init_theory_info name info = change_browser_info (fn (theories, files, tex_index, html_index, graph) => - (Symtab.curried_update (name, info) theories, files, tex_index, html_index, graph)); + (Symtab.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.curried_lookup theories name of + (case Symtab.lookup theories name of NONE => (warning ("Browser info: cannot access theory document " ^ quote name); info) - | SOME info => (Symtab.curried_update (name, map_theory_info f info) theories, files, + | SOME info => (Symtab.update (name, map_theory_info f info) theories, files, tex_index, html_index, graph))); diff -r 664434175578 -r e26cb20ef0cc src/Pure/Thy/thm_database.ML --- a/src/Pure/Thy/thm_database.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Thy/thm_database.ML Thu Sep 15 17:16:56 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.curried_lookup thms name)) = 1)) + SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1)) else NONE; val names = NameSpace.unpack name; in diff -r 664434175578 -r e26cb20ef0cc src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Thy/thm_deps.ML Thu Sep 15 17:16:56 2005 +0200 @@ -55,7 +55,7 @@ | _ => ["global"]); in if name mem parents' then (gra', parents union parents') - else (Symtab.curried_update (name, + else (Symtab.update (name, {name = Sign.base_name name, ID = name, dir = space_implode "/" (session @ prefx), unfold = false, path = "", parents = parents'}) gra', diff -r 664434175578 -r e26cb20ef0cc src/Pure/Thy/thy_parse.ML --- a/src/Pure/Thy/thy_parse.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Thy/thy_parse.ML Thu Sep 15 17:16:56 2005 +0200 @@ -469,7 +469,7 @@ end; fun sect tab ((Keyword, s, n) :: toks) = - (case Symtab.curried_lookup tab s of + (case Symtab.lookup tab s of SOME parse => !! parse toks | NONE => syn_err "section" s n) | sect _ ((_, s, n) :: _) = syn_err "section" s n diff -r 664434175578 -r e26cb20ef0cc src/Pure/Tools/am_interpreter.ML --- a/src/Pure/Tools/am_interpreter.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Tools/am_interpreter.ML Thu Sep 15 17:16:56 2005 +0200 @@ -107,7 +107,7 @@ fun match_closure prog clos = case len_head_of_closure 0 clos of (len, CConst c) => - (case prog_struct.lookup (prog, (c, len)) of + (case prog_struct.lookup prog (c, len) of NONE => NONE | SOME rules => match_rules 0 rules clos) | _ => NONE diff -r 664434175578 -r e26cb20ef0cc src/Pure/Tools/compute.ML --- a/src/Pure/Tools/compute.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/Tools/compute.ML Thu Sep 15 17:16:56 2005 +0200 @@ -44,13 +44,13 @@ val remove_types = let fun remove_types_var table invtable ccount vcount ldepth t = - (case Termtab.curried_lookup table t of + (case Termtab.lookup table t of NONE => let val a = AbstractMachine.Var vcount in - (Termtab.curried_update (t, a) table, - AMTermTab.curried_update (a, t) invtable, + (Termtab.update (t, a) table, + AMTermTab.update (a, t) invtable, ccount, inc vcount, AbstractMachine.Var (add vcount ldepth)) @@ -60,13 +60,13 @@ | SOME _ => sys_error "remove_types_var: lookup should be a var") fun remove_types_const table invtable ccount vcount ldepth t = - (case Termtab.curried_lookup table t of + (case Termtab.lookup table t of NONE => let val a = AbstractMachine.Const ccount in - (Termtab.curried_update (t, a) table, - AMTermTab.curried_update (a, t) invtable, + (Termtab.update (t, a) table, + AMTermTab.update (a, t) invtable, inc ccount, vcount, a) @@ -114,12 +114,12 @@ let fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) = if v < ldepth then (Bound v, List.nth (bounds, v)) else - (case AMTermTab.curried_lookup invtable (AbstractMachine.Var (v-ldepth)) of + (case AMTermTab.lookup invtable (AbstractMachine.Var (v-ldepth)) of SOME (t as Var (_, ty)) => (t, ty) | SOME (t as Free (_, ty)) => (t, ty) | _ => sys_error "infer_types: lookup should deliver Var or Free") | infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) = - (case AMTermTab.curried_lookup invtable c of + (case AMTermTab.lookup invtable c of SOME (c as Const (_, ty)) => (c, ty) | _ => sys_error "infer_types: lookup should deliver Const") | infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) = @@ -176,10 +176,10 @@ fun make_pattern table invtable n vars (var as AbstractMachine.Var v) = let - val var' = valOf (AMTermTab.curried_lookup invtable var) + val var' = valOf (AMTermTab.lookup invtable var) val table = Termtab.delete var' table val invtable = AMTermTab.delete var invtable - val vars = Inttab.curried_update_new (v, n) vars handle Inttab.DUP _ => + val vars = Inttab.update_new (v, n) vars handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed") in (table, invtable, n+1, vars, AbstractMachine.PVar) @@ -217,7 +217,7 @@ fun rename ldepth vars (var as AbstractMachine.Var v) = if v < ldepth then var - else (case Inttab.curried_lookup vars (v - ldepth) of + else (case Inttab.lookup vars (v - ldepth) of NONE => raise (Make "new variable on right hand side") | SOME n => AbstractMachine.Var ((vcount-n-1)+ldepth)) | rename ldepth vars (c as AbstractMachine.Const _) = c diff -r 664434175578 -r e26cb20ef0cc src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/axclass.ML Thu Sep 15 17:16:56 2005 +0200 @@ -148,7 +148,7 @@ (* get and put data *) -val lookup_info = Symtab.curried_lookup o AxclassesData.get; +val lookup_info = Symtab.lookup o AxclassesData.get; fun get_info thy c = (case lookup_info thy c of @@ -220,7 +220,7 @@ axms_thy |> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)) |> Theory.restore_naming class_thy - |> AxclassesData.map (Symtab.curried_update (class, info)); + |> AxclassesData.map (Symtab.update (class, info)); in (final_thy, {intro = intro, axioms = axioms}) end; in diff -r 664434175578 -r e26cb20ef0cc src/Pure/codegen.ML --- a/src/Pure/codegen.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/codegen.ML Thu Sep 15 17:16:56 2005 +0200 @@ -427,13 +427,13 @@ let val s' = NameSpace.pack ys val s'' = NameSpace.append module s' - in case Symtab.curried_lookup used s'' of + in case Symtab.lookup used s'' of NONE => ((module, s'), - (Symtab.curried_update_new (s, (module, s')) tab, - Symtab.curried_update_new (s'', ()) used)) + (Symtab.update_new (s, (module, s')) tab, + Symtab.update_new (s'', ()) used)) | SOME _ => find_name yss end - in case Symtab.curried_lookup tab s of + in case Symtab.lookup tab s of NONE => find_name (Library.suffixes1 (NameSpace.unpack s)) | SOME name => (name, p) end; @@ -453,7 +453,7 @@ in ((gr, (tab1', tab2)), (module, s'')) end; fun get_const_id cname (gr, (tab1, tab2)) = - case Symtab.curried_lookup (fst tab1) cname of + case Symtab.lookup (fst tab1) cname of NONE => error ("get_const_id: no such constant: " ^ quote cname) | SOME (module, s) => let @@ -469,7 +469,7 @@ in ((gr, (tab1, tab2')), (module, s'')) end; fun get_type_id tyname (gr, (tab1, tab2)) = - case Symtab.curried_lookup (fst tab2) tyname of + case Symtab.lookup (fst tab2) tyname of NONE => error ("get_type_id: no such type: " ^ quote tyname) | SOME (module, s) => let @@ -557,15 +557,15 @@ NONE => defs | SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of NONE => defs - | SOME (s, (T, (args, rhs))) => Symtab.curried_update + | SOME (s, (T, (args, rhs))) => Symtab.update (s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) :: - if_none (Symtab.curried_lookup defs s) []) defs)) + if_none (Symtab.lookup defs s) []) defs)) in foldl (fn ((thyname, axms), defs) => Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss end; -fun get_defn thy defs s T = (case Symtab.curried_lookup defs s of +fun get_defn thy defs s T = (case Symtab.lookup defs s of NONE => NONE | SOME ds => let val i = find_index (is_instance thy T o fst) ds @@ -829,7 +829,7 @@ (Graph.merge (fn ((_, module, _), (_, module', _)) => module = module') (gr, gr'), (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr - (map (fn s => case Symtab.curried_lookup graphs s of + (map (fn s => case Symtab.lookup graphs s of NONE => error ("Undefined code module: " ^ s) | SOME gr => gr) modules)) handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks); @@ -1056,7 +1056,7 @@ "use \"" ^ name ^ ".ML\";\n") code)) :: code) else File.write (Path.unpack fname) (snd (hd code))); if lib then thy - else map_modules (Symtab.curried_update (module, gr)) thy) + else map_modules (Symtab.update (module, gr)) thy) end)); val code_libraryP = diff -r 664434175578 -r e26cb20ef0cc src/Pure/compress.ML --- a/src/Pure/compress.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/compress.ML Thu Sep 15 17:16:56 2005 +0200 @@ -42,11 +42,11 @@ let val typs = #1 (CompressData.get thy); fun compress T = - (case Typtab.curried_lookup (! typs) T of + (case Typtab.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 (Typtab.curried_update (T', T')); T' end); + in change typs (Typtab.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.curried_lookup (! terms) t of + (case Termtab.lookup (! terms) t of SOME t' => t' - | NONE => (change terms (Termtab.curried_update (t, t)); t)); + | NONE => (change terms (Termtab.update (t, t)); t)); in compress o map_term_types (typ thy) end; end; diff -r 664434175578 -r e26cb20ef0cc src/Pure/context.ML --- a/src/Pure/context.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/context.ML Thu Sep 15 17:16:56 2005 +0200 @@ -118,7 +118,7 @@ val kinds = ref (Inttab.empty: kind Inttab.table); fun invoke meth_name meth_fn k = - (case Inttab.curried_lookup (! kinds) k of + (case Inttab.lookup (! kinds) k of SOME kind => meth_fn kind |> transform_failure (fn exn => EXCEPTION (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed")) | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k)); @@ -137,7 +137,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 _ = change kinds (Inttab.curried_update (k, kind)); + val _ = change kinds (Inttab.update (k, kind)); in k end; val copy_data = Inttab.map' invoke_copy; @@ -253,7 +253,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.curried_update id ids; + else Inttab.update id ids; fun check_insert intermediate id (ids, iids) = let val ids' = check_ins id ids and iids' = check_ins id iids @@ -420,12 +420,12 @@ val declare = declare_theory_data; fun get k dest thy = - (case Inttab.curried_lookup (#theory (data_of thy)) k of + (case Inttab.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 (Inttab.curried_update (k, mk x))); +fun put k mk x = modify_thy (map_theory (Inttab.update (k, mk x))); fun init k = put k I (invoke_empty k); end; @@ -522,7 +522,7 @@ val kinds = ref (Inttab.empty: kind Inttab.table); fun invoke meth_name meth_fn k = - (case Inttab.curried_lookup (! kinds) k of + (case Inttab.lookup (! kinds) k of SOME kind => meth_fn kind |> transform_failure (fn exn => EXCEPTION (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed")) | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k)); @@ -546,18 +546,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 _ = change kinds (Inttab.curried_update (k, kind)); + val _ = change kinds (Inttab.update (k, kind)); in k end; -fun init k = modify_thy (map_proof (Inttab.curried_update (k, ()))); +fun init k = modify_thy (map_proof (Inttab.update (k, ()))); fun get k dest prf = - (case Inttab.curried_lookup (data_of_proof prf) k of + (case Inttab.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 (Inttab.curried_update (k, mk x)); +fun put k mk x = map_prf (Inttab.update (k, mk x)); end; diff -r 664434175578 -r e26cb20ef0cc src/Pure/defs.ML --- a/src/Pure/defs.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/defs.ML Thu Sep 15 17:16:56 2005 +0200 @@ -46,11 +46,11 @@ typ (* type of the constant in this particular definition *) * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *) -fun getnode graph = the o Symtab.curried_lookup graph +fun getnode graph = the o Symtab.lookup graph fun get_nodedefs (Node (_, defs, _, _, _)) = defs -fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.curried_lookup defs defname +fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup defs defname fun get_defnode' graph noderef = - Symtab.curried_lookup (get_nodedefs (the (Symtab.curried_lookup graph noderef))) + Symtab.lookup (get_nodedefs (the (Symtab.lookup graph noderef))) fun table_size table = Symtab.fold (K (fn x => x + 1)) table 0; @@ -94,7 +94,7 @@ val tv = typ_tvars t val t' = Logic.incr_tvar inc t fun update_subst ((n, i), _) = - Vartab.curried_update ((n, i), ([], TVar ((n, i + inc), []))); + Vartab.update ((n, i), ([], TVar ((n, i + inc), []))); in (t', fold update_subst tv Vartab.empty) end @@ -157,9 +157,9 @@ ((tab,max), []) ts fun idx (tab,max) (TVar ((a,i),_)) = - (case Inttab.curried_lookup tab i of + (case Inttab.lookup tab i of SOME j => ((tab, max), TVar ((a,j),[])) - | NONE => ((Inttab.curried_update (i, max) tab, max + 1), TVar ((a,max),[]))) + | NONE => ((Inttab.update (i, max) tab, max + 1), TVar ((a,max),[]))) | idx (tab,max) (Type (t, ts)) = let val ((tab, max), ts) = idxlist idx I fst (tab, max) ts @@ -207,10 +207,10 @@ fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) = (cost, axmap, (Declare cty)::actions, - Symtab.curried_update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph) + Symtab.update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph) handle Symtab.DUP _ => let - val (Node (gty, _, _, _, _)) = the (Symtab.curried_lookup graph name) + val (Node (gty, _, _, _, _)) = the (Symtab.lookup graph name) in if is_instance_r ty gty andalso is_instance_r gty ty then g @@ -227,13 +227,13 @@ val _ = axcounter := c+1 val axname' = axname^"_"^(IntInf.toString c) in - (Symtab.curried_update (axname', axname) axmap, axname') + (Symtab.update (axname', axname) axmap, axname') end fun translate_ex axmap x = let fun translate (ty, nodename, axname) = - (ty, nodename, the (Symtab.curried_lookup axmap axname)) + (ty, nodename, the (Symtab.lookup axmap axname)) in case x of INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain)) @@ -243,7 +243,7 @@ fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body = let - val mainnode = (case Symtab.curried_lookup graph mainref of + val mainnode = (case Symtab.lookup graph mainref of NONE => def_err ("constant "^mainref^" is not declared") | SOME n => n) val (Node (gty, defs, backs, finals, _)) = mainnode @@ -273,8 +273,8 @@ let val links = map normalize_edge_idx links in - Symtab.curried_update (nodename, - case Symtab.curried_lookup edges nodename of + Symtab.update (nodename, + case Symtab.lookup edges nodename of NONE => links | SOME links' => merge_edges links' links) edges end) @@ -282,7 +282,7 @@ fun make_edges ((bodyn, bodyty), edges) = let val bnode = - (case Symtab.curried_lookup graph bodyn of + (case Symtab.lookup graph bodyn of NONE => def_err "body of constant definition references undeclared constant" | SOME x => x) val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode @@ -345,13 +345,13 @@ sys_error ("install_backrefs: closed node cannot be updated") else () val defnames = - (case Symtab.curried_lookup backs mainref of + (case Symtab.lookup backs mainref of NONE => Symtab.empty | SOME s => s) - val defnames' = Symtab.curried_update_new (axname, ()) defnames - val backs' = Symtab.curried_update (mainref, defnames') backs + val defnames' = Symtab.update_new (axname, ()) defnames + val backs' = Symtab.update (mainref, defnames') backs in - Symtab.curried_update (noderef, Node (ty, defs, backs', finals, closed)) graph + Symtab.update (noderef, Node (ty, defs, backs', finals, closed)) graph end else graph @@ -364,7 +364,7 @@ else if closed = Open andalso is_instance_r gty ty then Closed else closed val thisDefnode = Defnode (ty, edges) - val graph = Symtab.curried_update (mainref, Node (gty, Symtab.curried_update_new + val graph = Symtab.update (mainref, Node (gty, Symtab.update_new (axname, thisDefnode) defs, backs, finals, closed)) graph (* Now we have to check all backreferences to this node and inform them about @@ -377,8 +377,8 @@ getnode graph noderef val _ = if closed = Final then sys_error "update_defs: closed node" else () val (Defnode (def_ty, defnode_edges)) = - the (Symtab.curried_lookup nodedefs defname) - val edges = the (Symtab.curried_lookup defnode_edges mainref) + the (Symtab.lookup nodedefs defname) + val edges = the (Symtab.lookup defnode_edges mainref) val refclosed = ref false (* the type of thisDefnode is ty *) @@ -416,7 +416,7 @@ val defnames' = if edges' = [] then defnames else - Symtab.curried_update (defname, ()) defnames + Symtab.update (defname, ()) defnames in if changed then let @@ -424,14 +424,14 @@ if edges' = [] then Symtab.delete mainref defnode_edges else - Symtab.curried_update (mainref, edges') defnode_edges + Symtab.update (mainref, edges') defnode_edges val defnode' = Defnode (def_ty, defnode_edges') - val nodedefs' = Symtab.curried_update (defname, defnode') nodedefs + val nodedefs' = Symtab.update (defname, defnode') nodedefs val closed = if closed = Closed andalso Symtab.is_empty defnode_edges' andalso no_forwards nodedefs' then Final else closed val graph' = - Symtab.curried_update + Symtab.update (noderef, Node (nodety, nodedefs', nodebacks, nodefinals, closed)) graph in (defnames', graph') @@ -447,7 +447,7 @@ (backs, graph') else let - val backs' = Symtab.curried_update_new (noderef, defnames') backs + val backs' = Symtab.update_new (noderef, defnames') backs in (backs', graph') end @@ -458,7 +458,7 @@ (* If a Circular exception is thrown then we never reach this point. *) val (Node (gty, defs, _, finals, closed)) = getnode graph mainref val closed = if closed = Closed andalso no_forwards defs then Final else closed - val graph = Symtab.curried_update (mainref, Node (gty, defs, backs, finals, closed)) graph + val graph = Symtab.update (mainref, Node (gty, defs, backs, finals, closed)) graph val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions in (cost+3, axmap, actions', graph) @@ -482,7 +482,7 @@ end fun finalize' (cost, axmap, history, graph) (noderef, ty) = - case Symtab.curried_lookup graph noderef of + case Symtab.lookup graph noderef of NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared") | SOME (Node (nodety, defs, backs, finals, closed)) => let @@ -519,7 +519,7 @@ val closed = if closed = Open andalso is_instance_r nodety ty then Closed else closed - val graph = Symtab.curried_update (noderef, Node (nodety, defs, backs, finals, closed)) graph + val graph = Symtab.update (noderef, Node (nodety, defs, backs, finals, closed)) graph fun update_backref ((graph, backs), (backrefname, backdefnames)) = let @@ -532,7 +532,7 @@ the (get_defnode backnode backdefname) val (defnames', all_edges') = - case Symtab.curried_lookup all_edges noderef of + case Symtab.lookup all_edges noderef of NONE => sys_error "finalize: corrupt backref" | SOME edges => let @@ -542,11 +542,11 @@ if edges' = [] then (defnames, Symtab.delete noderef all_edges) else - (Symtab.curried_update (backdefname, ()) defnames, - Symtab.curried_update (noderef, edges') all_edges) + (Symtab.update (backdefname, ()) defnames, + Symtab.update (noderef, edges') all_edges) end val defnode' = Defnode (def_ty, all_edges') - val backdefs' = Symtab.curried_update (backdefname, defnode') backdefs + val backdefs' = Symtab.update (backdefname, defnode') backdefs val backclosed' = if backclosed = Closed andalso Symtab.is_empty all_edges' andalso no_forwards backdefs' @@ -554,19 +554,19 @@ val backnode' = Node (backty, backdefs', backbacks, backfinals, backclosed') in - (Symtab.curried_update (backrefname, backnode') graph, defnames') + (Symtab.update (backrefname, backnode') graph, defnames') end val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames) in (graph', if Symtab.is_empty defnames' then backs - else Symtab.curried_update (backrefname, defnames') backs) + else Symtab.update (backrefname, defnames') backs) end val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) val Node ( _, defs, _, _, closed) = getnode graph' noderef val closed = if closed = Closed andalso no_forwards defs then Final else closed - val graph' = Symtab.curried_update (noderef, Node (nodety, defs, backs', + val graph' = Symtab.update (noderef, Node (nodety, defs, backs', finals, closed)) graph' val history' = (Finalize (noderef, ty)) :: history in @@ -577,14 +577,14 @@ fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty) fun update_axname ax orig_ax (cost, axmap, history, graph) = - (cost, Symtab.curried_update (ax, orig_ax) axmap, history, graph) + (cost, Symtab.update (ax, orig_ax) axmap, history, graph) fun merge' (Declare cty, g) = declare' g cty | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) = - (case Symtab.curried_lookup graph name of + (case Symtab.lookup graph name of NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body | SOME (Node (_, defs, _, _, _)) => - (case Symtab.curried_lookup defs axname of + (case Symtab.lookup defs axname of NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body | SOME _ => g)) | merge' (Finalize finals, g) = finalize' g finals @@ -598,14 +598,14 @@ fun finals (_, _, history, graph) = Symtab.foldl (fn (finals, (name, Node(_, _, _, ftys, _))) => - Symtab.curried_update_new (name, ftys) finals) + Symtab.update_new (name, ftys) finals) (Symtab.empty, graph) fun overloading_info (_, axmap, _, graph) c = let - fun translate (ax, Defnode (ty, _)) = (the (Symtab.curried_lookup axmap ax), ty) + fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup axmap ax), ty) in - case Symtab.curried_lookup graph c of + case Symtab.lookup graph c of NONE => NONE | SOME (Node (ty, defnodes, _, _, state)) => SOME (ty, map translate (Symtab.dest defnodes), state) @@ -618,7 +618,7 @@ | monomorphicT _ = false fun monomorphic (_, _, _, graph) c = - (case Symtab.curried_lookup graph c of + (case Symtab.lookup graph c of NONE => true | SOME (Node (ty, defnodes, _, _, _)) => Symtab.min_key defnodes = Symtab.max_key defnodes andalso diff -r 664434175578 -r e26cb20ef0cc src/Pure/envir.ML --- a/src/Pure/envir.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/envir.ML Thu Sep 15 17:16:56 2005 +0200 @@ -73,7 +73,7 @@ [T', T], []); fun gen_lookup f asol (xname, T) = - (case Vartab.curried_lookup asol xname of + (case Vartab.lookup asol xname of NONE => NONE | SOME (U, t) => if f (T, U) then SOME t else var_clash xname T U); @@ -92,7 +92,7 @@ fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p; fun update (((xname, T), t), Envir {maxidx, asol, iTs}) = - Envir{maxidx=maxidx, asol=Vartab.curried_update_new (xname, (T, t)) asol, iTs=iTs}; + Envir{maxidx=maxidx, asol=Vartab.update_new (xname, (T, t)) asol, iTs=iTs}; (*The empty environment. New variables will start with the given index+1.*) fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty}; diff -r 664434175578 -r e26cb20ef0cc src/Pure/fact_index.ML --- a/src/Pure/fact_index.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/fact_index.ML Thu Sep 15 17:16:56 2005 +0200 @@ -55,7 +55,7 @@ fun add pred (name, ths) (Index {next, facts, consts, frees}) = let - fun upd a = Symtab.curried_update_multi (a, (next, (name, ths))); + fun upd a = Symtab.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 (Symtab.curried_lookup_multi consts) cs @ - map (Symtab.curried_lookup_multi frees) xs) |> intersects |> map #2; + (map (Symtab.lookup_multi consts) cs @ + map (Symtab.lookup_multi frees) xs) |> intersects |> map #2; end; diff -r 664434175578 -r e26cb20ef0cc src/Pure/goals.ML --- a/src/Pure/goals.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/goals.ML Thu Sep 15 17:16:56 2005 +0200 @@ -213,13 +213,13 @@ (* access locales *) -val get_locale = Symtab.curried_lookup o #locales o LocalesData.get; +val get_locale = Symtab.lookup o #locales o LocalesData.get; fun put_locale (name, locale) thy = let val {space, locales, scope} = LocalesData.get thy; val space' = Sign.declare_name thy name space; - val locales' = Symtab.curried_update (name, locale) locales; + val locales' = Symtab.update (name, locale) locales; in thy |> LocalesData.put (make_locale_data space' locales' scope) end; fun lookup_locale thy xname = diff -r 664434175578 -r e26cb20ef0cc src/Pure/net.ML --- a/src/Pure/net.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/net.ML Thu Sep 15 17:16:56 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.curried_lookup atoms a) empty; - val atoms' = Symtab.curried_update (a, ins1 (keys, net')) atoms; + val net' = if_none (Symtab.lookup atoms a) empty; + val atoms' = Symtab.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.curried_lookup atoms a of + (case Symtab.lookup atoms a of NONE => raise DELETE | SOME net' => (case del1 (keys, net') of Leaf [] => Symtab.delete a atoms - | net'' => Symtab.curried_update (a, net'') atoms)) + | net'' => Symtab.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.curried_lookup atoms a of + (case Symtab.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.curried_lookup atoms1 a) emptynet) net) atoms2 + subtr (if_none (Symtab.lookup atoms1 a) emptynet) net) atoms2 in subtr net1 net2 [] end; fun entries net = subtract (K false) empty net; diff -r 664434175578 -r e26cb20ef0cc src/Pure/pattern.ML --- a/src/Pure/pattern.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/pattern.ML Thu Sep 15 17:16:56 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.curried_update_new (ixn, (T, t)) insts) + Vartab.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.curried_update_new (ixn, (T, t)) itms else raise MATCH + then if null js then Vartab.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.curried_update_new (ixn, (T, mkabs (binders, is, t'))) itms end + in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end else raise MATCH end; diff -r 664434175578 -r e26cb20ef0cc src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/proofterm.ML Thu Sep 15 17:16:56 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.curried_lookup thms name of - NONE => oras_of prf (Symtab.curried_update (name, [prop]) thms, oras) + case Symtab.lookup thms name of + NONE => oras_of prf (Symtab.update (name, [prop]) thms, oras) | SOME ps => if prop mem ps then tabs else - oras_of prf (Symtab.curried_update (name, prop::ps) thms, oras)) + oras_of prf (Symtab.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.curried_lookup tab s of - NONE => thms_of_proof prf (Symtab.curried_update (s, [(prop, prf')]) tab) + case Symtab.lookup tab s of + NONE => thms_of_proof prf (Symtab.update (s, [(prop, prf')]) tab) | SOME ps => if exists (equal prop o fst) ps then tab else - thms_of_proof prf (Symtab.curried_update (s, (prop, prf')::ps) tab)) + thms_of_proof prf (Symtab.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, _, _)) = Symtab.curried_update (s, prf) + | axms_of_proof (prf as PAxm (s, _, _)) = Symtab.update (s, prf) | axms_of_proof (MinProof (_, prfs, _)) = fold (axms_of_proof o proof_of_min_axm) prfs | axms_of_proof _ = I; diff -r 664434175578 -r e26cb20ef0cc src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/sign.ML Thu Sep 15 17:16:56 2005 +0200 @@ -285,8 +285,8 @@ fun const_constraint thy c = let val ((_, consts), constraints) = #consts (rep_sg thy) in - (case Symtab.curried_lookup constraints c of - NONE => Option.map #1 (Symtab.curried_lookup consts c) + (case Symtab.lookup constraints c of + NONE => Option.map #1 (Symtab.lookup consts c) | some => some) end; @@ -294,7 +294,7 @@ (case const_constraint thy c of SOME T => T | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], [])); -val const_type = Option.map #1 oo (Symtab.curried_lookup o #2 o #1 o #consts o rep_sg); +val const_type = Option.map #1 oo (Symtab.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 @@ -517,7 +517,7 @@ fun read_tyname thy raw_c = let val c = intern_type thy raw_c in - (case Symtab.curried_lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of + (case Symtab.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; @@ -717,7 +717,7 @@ handle TYPE (msg, _, _) => error msg; val _ = cert_term thy (Const (c, T)) handle TYPE (msg, _, _) => error msg; - in thy |> map_consts (apsnd (Symtab.curried_update (c, T))) end; + in thy |> map_consts (apsnd (Symtab.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 664434175578 -r e26cb20ef0cc src/Pure/sorts.ML --- a/src/Pure/sorts.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/sorts.ML Thu Sep 15 17:16:56 2005 +0200 @@ -180,7 +180,7 @@ fun mg_domain (classes, arities) a S = let fun dom c = - (case AList.lookup (op =) (Symtab.curried_lookup_multi arities a) c of + (case AList.lookup (op =) (Symtab.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 664434175578 -r e26cb20ef0cc src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/thm.ML Thu Sep 15 17:16:56 2005 +0200 @@ -526,7 +526,7 @@ fun get_axiom_i theory name = let fun get_ax thy = - Symtab.curried_lookup (#2 (#axioms (Theory.rep_theory thy))) name + Symtab.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), @@ -1484,7 +1484,7 @@ fun invoke_oracle_i thy1 name = let val oracle = - (case Symtab.curried_lookup (#2 (#oracles (Theory.rep_theory thy1))) name of + (case Symtab.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 664434175578 -r e26cb20ef0cc src/Pure/type.ML --- a/src/Pure/type.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/Pure/type.ML Thu Sep 15 17:16:56 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.curried_lookup types c of + (case Symtab.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.curried_lookup tye ixn of + (case Vartab.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.curried_update_new (v, (S, T)) subs + if of_sort tsig (T, S) then Vartab.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.curried_update_new (v, (S, T)) subs + NONE => Vartab.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,7 +366,7 @@ fun meet (_, []) tye = tye | meet (TVar (xi, S'), S) tye = if Sorts.sort_le classes (S', S) then tye - else Vartab.curried_update_new + else Vartab.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 @@ -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.curried_update_new (w, (S2, T)) tye + Vartab.update_new (w, (S2, T)) tye else if Sorts.sort_le classes (S2, S1) then - Vartab.curried_update_new (v, (S1, U)) tye + Vartab.update_new (v, (S1, U)) tye else let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in - Vartab.curried_update_new (v, (S1, S)) (Vartab.curried_update_new (w, (S2, S)) tye) + Vartab.update_new (v, (S1, S)) (Vartab.update_new (w, (S2, S)) tye) end | (TVar (v, S), T) => if occurs v tye T then raise TUNIFY - else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye) + else meet (T, S) (Vartab.update_new (v, (S, T)) tye) | (T, TVar (v, S)) => if occurs v tye T then raise TUNIFY - else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye) + else meet (T, S) (Vartab.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.curried_update_new (w, (S2, T)) tye + else Vartab.update_new (w, (S2, T)) tye | (TVar (v, S), T) => if occurs v tye T then raise TUNIFY - else Vartab.curried_update_new (v, (S, T)) tye + else Vartab.update_new (v, (S, T)) tye | (T, TVar (v, S)) => if occurs v tye T then raise TUNIFY - else Vartab.curried_update_new (v, (S, T)) tye + else Vartab.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.curried_lookup_multi arities t + Symtab.lookup_multi arities t |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars) - in Symtab.curried_update (t, ars') arities end; + in Symtab.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.curried_lookup (#2 types) t of + (case Symtab.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.curried_lookup types c' of + (case Symtab.lookup types c' of SOME (decl', _) => err_in_decls c' decl decl' - | NONE => Symtab.curried_update (c', (decl, stamp ())) types); + | NONE => Symtab.update (c', (decl, stamp ())) types); in (space', types') end; -fun the_decl (_, types) = fst o the o Symtab.curried_lookup types; +fun the_decl (_, types) = fst o the o Symtab.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.curried_lookup types c of SOME (Nonterminal, _) => true | _ => false) + (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false) orelse exists (syntactic types) Ts | syntactic _ _ = false; diff -r 664434175578 -r e26cb20ef0cc src/ZF/Datatype.ML --- a/src/ZF/Datatype.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/ZF/Datatype.ML Thu Sep 15 17:16:56 2005 +0200 @@ -73,9 +73,9 @@ and (rhead, rargs) = strip_comb rhs val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; val rname = #1 (dest_Const rhead) handle TERM _ => raise Match; - val lcon_info = the (Symtab.curried_lookup (ConstructorsData.get sg) lname) + val lcon_info = the (Symtab.lookup (ConstructorsData.get sg) lname) handle Option => raise Match; - val rcon_info = the (Symtab.curried_lookup (ConstructorsData.get sg) rname) + val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname) handle Option => raise Match; val new = if #big_rec_name lcon_info = #big_rec_name rcon_info diff -r 664434175578 -r e26cb20ef0cc src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/ZF/Tools/datatype_package.ML Thu Sep 15 17:16:56 2005 +0200 @@ -383,8 +383,8 @@ (("recursor_eqns", recursor_eqns), []), (("free_iffs", free_iffs), []), (("free_elims", free_SEs), [])]) - |> DatatypesData.map (Symtab.curried_update (big_rec_name, dt_info)) - |> ConstructorsData.map (fold Symtab.curried_update con_pairs) + |> DatatypesData.map (Symtab.update (big_rec_name, dt_info)) + |> ConstructorsData.map (fold Symtab.update con_pairs) |> Theory.parent_path, ind_result, {con_defs = con_defs, diff -r 664434175578 -r e26cb20ef0cc src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/ZF/Tools/ind_cases.ML Thu Sep 15 17:16:56 2005 +0200 @@ -31,7 +31,7 @@ end); -fun declare name f = IndCasesData.map (Symtab.curried_update (name, f)); +fun declare name f = IndCasesData.map (Symtab.update (name, f)); fun smart_cases thy ss read_prop s = let @@ -40,7 +40,7 @@ val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop (Logic.strip_imp_concl A)))))) handle TERM _ => err (); in - (case Symtab.curried_lookup (IndCasesData.get thy) c of + (case Symtab.lookup (IndCasesData.get thy) c of NONE => error ("Unknown inductive cases rule for set " ^ quote c) | SOME f => f ss (Thm.cterm_of (Theory.sign_of thy) A)) end; diff -r 664434175578 -r e26cb20ef0cc src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/ZF/Tools/induct_tacs.ML Thu Sep 15 17:16:56 2005 +0200 @@ -70,7 +70,7 @@ struct fun datatype_info thy name = - (case Symtab.curried_lookup (DatatypesData.get thy) name of + (case Symtab.lookup (DatatypesData.get thy) name of SOME info => info | NONE => error ("Unknown datatype " ^ quote name)); @@ -166,8 +166,8 @@ thy |> Theory.add_path (Sign.base_name big_rec_name) |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]) - |> DatatypesData.put (Symtab.curried_update (big_rec_name, dt_info) (DatatypesData.get thy)) - |> ConstructorsData.put (fold_rev Symtab.curried_update con_pairs (ConstructorsData.get thy)) + |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy)) + |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy)) |> Theory.parent_path end; diff -r 664434175578 -r e26cb20ef0cc src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Thu Sep 15 17:16:55 2005 +0200 +++ b/src/ZF/Tools/primrec_package.ML Thu Sep 15 17:16:56 2005 +0200 @@ -56,7 +56,7 @@ else strip_comb (hd middle); val (cname, _) = dest_Const constr handle TERM _ => raise RecError "ill-formed constructor"; - val con_info = the (Symtab.curried_lookup (ConstructorsData.get thy) cname) + val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname) handle Option => raise RecError "cannot determine datatype associated with function"