--- 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
--- 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
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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))
--- 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 => []
--- 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
--- 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, ...}) =>
--- 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
--- 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)) |>
--- 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
--- 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
--- 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;
--- 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
--- 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;
--- 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 []
--- 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
--- 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 *)
--- 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);
--- 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;
--- 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
--- 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*)
--- 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);
--- 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
--- 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);
--- 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;
--- 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 *)
--- 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;
--- 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'));
--- 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
--- 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;
--- 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 ());
--- 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. *)
--- 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;
--- 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);
--- 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);
--- 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];
--- 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
--- 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
--- 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;
--- 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"
--- 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 =
--- 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);
--- 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
--- 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;
--- 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 "<sub>" "</sub>") (output_sym s);
--- 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)));
--- 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
--- 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',
--- 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
--- 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
--- 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
--- 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
--- 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 =
--- 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;
--- 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;
--- 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
--- 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};
--- 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;
--- 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 =
--- 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;
--- 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;
--- 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;
--- 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;
--- 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);
--- 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;
--- 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;
--- 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
--- 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,
--- 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;
--- 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;
--- 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"