TableFun/Symtab: curried lookup and update;
authorwenzelm
Thu Sep 15 17:16:56 2005 +0200 (2005-09-15 ago)
changeset 17412e26cb20ef0cc
parent 17411 664434175578
child 17413 89ccb3799428
TableFun/Symtab: curried lookup and update;
TFL/casesplit.ML
TFL/thry.ML
src/HOL/Import/hol4rews.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Matrix/cplex/CplexMatrixConverter.ML
src/HOL/Matrix/cplex/Cplex_tools.ML
src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
src/HOL/Matrix/cplex/fspmlp.ML
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/typedef_package.ML
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/combine_numerals.ML
src/Provers/Arith/extract_common_term.ML
src/Pure/General/graph.ML
src/Pure/General/name_space.ML
src/Pure/General/output.ML
src/Pure/General/symbol.ML
src/Pure/General/table.ML
src/Pure/IsaPlanner/term_lib.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_output.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/term_style.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/proofchecker.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/html.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thm_database.ML
src/Pure/Thy/thm_deps.ML
src/Pure/Thy/thy_parse.ML
src/Pure/Tools/am_interpreter.ML
src/Pure/Tools/compute.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/compress.ML
src/Pure/context.ML
src/Pure/defs.ML
src/Pure/envir.ML
src/Pure/fact_index.ML
src/Pure/goals.ML
src/Pure/net.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
src/Pure/sign.ML
src/Pure/sorts.ML
src/Pure/thm.ML
src/Pure/type.ML
src/ZF/Datatype.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/TFL/casesplit.ML	Thu Sep 15 17:16:55 2005 +0200
     1.2 +++ b/TFL/casesplit.ML	Thu Sep 15 17:16:56 2005 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4                                              ("Free type: " ^ s)
     1.5                     | TVar((s,i),_) => raise ERROR_MESSAGE
     1.6                                              ("Free variable: " ^ s)
     1.7 -      val dt = case Symtab.curried_lookup dtypestab ty_str
     1.8 +      val dt = case Symtab.lookup dtypestab ty_str
     1.9                  of SOME dt => dt
    1.10                   | NONE => raise ERROR_MESSAGE ("Not a Datatype: " ^ ty_str)
    1.11      in
     2.1 --- a/TFL/thry.ML	Thu Sep 15 17:16:55 2005 +0200
     2.2 +++ b/TFL/thry.ML	Thu Sep 15 17:16:56 2005 +0200
     2.3 @@ -59,7 +59,7 @@
     2.4   * Get information about datatypes
     2.5   *---------------------------------------------------------------------------*)
     2.6  
     2.7 -val get_info = Symtab.curried_lookup o DatatypePackage.get_datatypes;
     2.8 +val get_info = Symtab.lookup o DatatypePackage.get_datatypes;
     2.9  
    2.10  fun match_info thy tname =
    2.11    case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
     3.1 --- a/src/HOL/Import/hol4rews.ML	Thu Sep 15 17:16:55 2005 +0200
     3.2 +++ b/src/HOL/Import/hol4rews.ML	Thu Sep 15 17:16:56 2005 +0200
     3.3 @@ -110,12 +110,12 @@
     3.4  structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs);
     3.5  
     3.6  fun get_segment2 thyname thy =
     3.7 -  Symtab.curried_lookup (HOL4Imports.get thy) thyname
     3.8 +  Symtab.lookup (HOL4Imports.get thy) thyname
     3.9  
    3.10  fun set_segment thyname segname thy =
    3.11      let
    3.12  	val imps = HOL4Imports.get thy
    3.13 -	val imps' = Symtab.curried_update_new (thyname,segname) imps
    3.14 +	val imps' = Symtab.update_new (thyname,segname) imps
    3.15      in
    3.16  	HOL4Imports.put imps' thy
    3.17      end
    3.18 @@ -273,7 +273,7 @@
    3.19      let
    3.20  	val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
    3.21  	val curmaps = HOL4Maps.get thy
    3.22 -	val newmaps = StringPair.update_new(((bthy,bthm),NONE),curmaps)
    3.23 +	val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps
    3.24  	val upd_thy = HOL4Maps.put newmaps thy
    3.25      in
    3.26  	upd_thy
    3.27 @@ -291,19 +291,19 @@
    3.28  fun add_hol4_move bef aft thy =
    3.29      let
    3.30  	val curmoves = HOL4Moves.get thy
    3.31 -	val newmoves = Symtab.curried_update_new (bef, aft) curmoves
    3.32 +	val newmoves = Symtab.update_new (bef, aft) curmoves
    3.33      in
    3.34  	HOL4Moves.put newmoves thy
    3.35      end
    3.36  
    3.37  fun get_hol4_move bef thy =
    3.38 -  Symtab.curried_lookup (HOL4Moves.get thy) bef
    3.39 +  Symtab.lookup (HOL4Moves.get thy) bef
    3.40  
    3.41  fun follow_name thmname thy =
    3.42      let
    3.43  	val moves = HOL4Moves.get thy
    3.44  	fun F thmname =
    3.45 -	    case Symtab.curried_lookup moves thmname of
    3.46 +	    case Symtab.lookup moves thmname of
    3.47  		SOME name => F name
    3.48  	      | NONE => thmname
    3.49      in
    3.50 @@ -313,19 +313,19 @@
    3.51  fun add_hol4_cmove bef aft thy =
    3.52      let
    3.53  	val curmoves = HOL4CMoves.get thy
    3.54 -	val newmoves = Symtab.curried_update_new (bef, aft) curmoves
    3.55 +	val newmoves = Symtab.update_new (bef, aft) curmoves
    3.56      in
    3.57  	HOL4CMoves.put newmoves thy
    3.58      end
    3.59  
    3.60  fun get_hol4_cmove bef thy =
    3.61 -  Symtab.curried_lookup (HOL4CMoves.get thy) bef
    3.62 +  Symtab.lookup (HOL4CMoves.get thy) bef
    3.63  
    3.64  fun follow_cname thmname thy =
    3.65      let
    3.66  	val moves = HOL4CMoves.get thy
    3.67  	fun F thmname =
    3.68 -	    case Symtab.curried_lookup moves thmname of
    3.69 +	    case Symtab.lookup moves thmname of
    3.70  		SOME name => F name
    3.71  	      | NONE => thmname
    3.72      in
    3.73 @@ -337,7 +337,7 @@
    3.74  	val isathm = follow_name isathm thy
    3.75  	val _ = message ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)
    3.76  	val curmaps = HOL4Maps.get thy
    3.77 -	val newmaps = StringPair.update_new(((bthy,bthm),SOME isathm),curmaps)
    3.78 +	val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps
    3.79  	val upd_thy = HOL4Maps.put newmaps thy
    3.80      in
    3.81  	upd_thy
    3.82 @@ -347,14 +347,14 @@
    3.83      let
    3.84  	val maps = HOL4TypeMaps.get thy
    3.85      in
    3.86 -	StringPair.lookup(maps,(bthy,tycon))
    3.87 +	StringPair.lookup maps (bthy,tycon)
    3.88      end
    3.89  
    3.90  fun get_hol4_mapping bthy bthm thy =
    3.91      let
    3.92  	val curmaps = HOL4Maps.get thy
    3.93      in
    3.94 -	StringPair.lookup(curmaps,(bthy,bthm))
    3.95 +	StringPair.lookup curmaps (bthy,bthm)
    3.96      end;
    3.97  
    3.98  fun add_hol4_const_mapping bthy bconst internal isaconst thy =
    3.99 @@ -366,7 +366,7 @@
   3.100  				    else thy
   3.101  	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   3.102  	val curmaps = HOL4ConstMaps.get thy
   3.103 -	val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst,NONE)),curmaps)
   3.104 +	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps
   3.105  	val upd_thy = HOL4ConstMaps.put newmaps thy
   3.106      in
   3.107  	upd_thy
   3.108 @@ -376,7 +376,7 @@
   3.109      let
   3.110  	val currens = HOL4Rename.get thy
   3.111  	val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)
   3.112 -	val newrens = StringPair.update_new(((bthy,bconst),newname),currens)
   3.113 +	val newrens = StringPair.update_new ((bthy,bconst),newname) currens
   3.114  	val upd_thy = HOL4Rename.put newrens thy
   3.115      in
   3.116  	upd_thy
   3.117 @@ -386,7 +386,7 @@
   3.118      let
   3.119  	val currens = HOL4Rename.get thy
   3.120      in
   3.121 -	StringPair.lookup(currens,(bthy,bconst))
   3.122 +	StringPair.lookup currens (bthy,bconst)
   3.123      end;
   3.124  
   3.125  fun get_hol4_const_mapping bthy bconst thy =
   3.126 @@ -396,7 +396,7 @@
   3.127  		       | NONE => bconst
   3.128  	val maps = HOL4ConstMaps.get thy
   3.129      in
   3.130 -	StringPair.lookup(maps,(bthy,bconst))
   3.131 +	StringPair.lookup maps (bthy,bconst)
   3.132      end
   3.133  
   3.134  fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =
   3.135 @@ -408,7 +408,7 @@
   3.136  				    else thy
   3.137  	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   3.138  	val curmaps = HOL4ConstMaps.get thy
   3.139 -	val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst,SOME typ)),curmaps)
   3.140 +	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps
   3.141  	val upd_thy = HOL4ConstMaps.put newmaps thy
   3.142      in
   3.143  	upd_thy
   3.144 @@ -418,8 +418,8 @@
   3.145      let
   3.146  	val curmaps = HOL4TypeMaps.get thy
   3.147  	val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   3.148 -	val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst)),curmaps)
   3.149 -               handle x => let val (internal, isaconst') = the (StringPair.lookup (curmaps, (bthy, bconst))) in
   3.150 +	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
   3.151 +               handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
   3.152                        warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
   3.153          val upd_thy = HOL4TypeMaps.put newmaps thy
   3.154      in
   3.155 @@ -431,7 +431,7 @@
   3.156  	val thmname = Sign.full_name (sign_of thy) bthm
   3.157  	val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
   3.158  	val curpend = HOL4Pending.get thy
   3.159 -	val newpend = StringPair.update_new(((bthy,bthm),hth),curpend)
   3.160 +	val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
   3.161  	val upd_thy = HOL4Pending.put newpend thy
   3.162  	val thy' = case opt_get_output_thy upd_thy of
   3.163  		       "" => add_hol4_mapping bthy bthm thmname upd_thy
   3.164 @@ -450,14 +450,14 @@
   3.165      let
   3.166  	val isathms = HOL4Thms.get thy
   3.167      in
   3.168 -	StringPair.lookup (isathms,(thyname,thmname))
   3.169 +	StringPair.lookup isathms (thyname,thmname)
   3.170      end
   3.171  
   3.172  fun add_hol4_theorem thyname thmname hth thy =
   3.173      let
   3.174  	val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
   3.175  	val isathms = HOL4Thms.get thy
   3.176 -	val isathms' = StringPair.update_new (((thyname,thmname),hth),isathms)
   3.177 +	val isathms' = StringPair.update_new ((thyname,thmname),hth) isathms
   3.178  	val thy' = HOL4Thms.put isathms' thy
   3.179      in
   3.180  	thy'
   3.181 @@ -692,14 +692,14 @@
   3.182      let
   3.183  	val maps = HOL4DefMaps.get thy
   3.184      in
   3.185 -	StringPair.lookup(maps,(thyname,const))
   3.186 +	StringPair.lookup maps (thyname,const)
   3.187      end
   3.188  
   3.189  fun add_defmap thyname const defname thy =
   3.190      let
   3.191  	val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
   3.192  	val maps = HOL4DefMaps.get thy
   3.193 -	val maps' = StringPair.update_new(((thyname,const),defname),maps)
   3.194 +	val maps' = StringPair.update_new ((thyname,const),defname) maps
   3.195  	val thy' = HOL4DefMaps.put maps' thy
   3.196      in
   3.197  	thy'
   3.198 @@ -710,7 +710,7 @@
   3.199  	val maps = HOL4DefMaps.get thy
   3.200  	fun F dname = (dname,add_defmap thyname name dname thy)
   3.201      in
   3.202 -	case StringPair.lookup(maps,(thyname,name)) of
   3.203 +	case StringPair.lookup maps (thyname,name) of
   3.204  	    SOME thmname => (thmname,thy)
   3.205  	  | NONE =>
   3.206  	    let
     4.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Sep 15 17:16:55 2005 +0200
     4.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Sep 15 17:16:56 2005 +0200
     4.3 @@ -420,7 +420,7 @@
     4.4  	val name = intern_const_name Thy Nam thy
     4.5  	val cmaps = HOL4ConstMaps.get thy
     4.6      in
     4.7 -	case StringPair.lookup(cmaps,(Thy,Nam)) of
     4.8 +	case StringPair.lookup cmaps (Thy,Nam) of
     4.9  	    SOME(_,_,SOME ty) => Const(name,ty)
    4.10  	  | _ => get_const (sign_of thy) Thy name
    4.11      end
    4.12 @@ -1081,7 +1081,7 @@
    4.13  	let
    4.14  	    val pending = HOL4Pending.get thy
    4.15  	in
    4.16 -	    case StringPair.lookup (pending,(thyname,thmname)) of
    4.17 +	    case StringPair.lookup pending (thyname,thmname) of
    4.18  		SOME hth => SOME (HOLThm hth)
    4.19  	      | NONE => NONE
    4.20  	end
     5.1 --- a/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Thu Sep 15 17:16:55 2005 +0200
     5.2 +++ b/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Thu Sep 15 17:16:56 2005 +0200
     5.3 @@ -57,14 +57,14 @@
     5.4      let	
     5.5  	fun build_naming index i2s s2i [] = (index, i2s, s2i)
     5.6  	  | build_naming index i2s s2i (cplexBounds (cplexNeg cplexInf, cplexLeq, cplexVar v, cplexLeq, cplexInf)::bounds)
     5.7 -	    = build_naming (index+1) (Inttab.curried_update (index, v) i2s) (Symtab.curried_update_new (v, index) s2i) bounds
     5.8 +	    = build_naming (index+1) (Inttab.update (index, v) i2s) (Symtab.update_new (v, index) s2i) bounds
     5.9  	  | build_naming _ _ _ _ = raise (Converter "nonfree bound")
    5.10  
    5.11  	val (varcount, i2s_tab, s2i_tab) = build_naming 0 Inttab.empty Symtab.empty bounds
    5.12  
    5.13 -	fun i2s i = case Inttab.curried_lookup i2s_tab i of NONE => raise (Converter "index not found")
    5.14 +	fun i2s i = case Inttab.lookup i2s_tab i of NONE => raise (Converter "index not found")
    5.15  						     | SOME n => n
    5.16 -	fun s2i s = case Symtab.curried_lookup s2i_tab s of NONE => raise (Converter ("name not found: "^s))
    5.17 +	fun s2i s = case Symtab.lookup s2i_tab s of NONE => raise (Converter ("name not found: "^s))
    5.18  						     | SOME i => i
    5.19  	fun num2str positive (cplexNeg t) = num2str (not positive) t
    5.20  	  | num2str positive (cplexNum num) = if positive then num else "-"^num			
     6.1 --- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Thu Sep 15 17:16:55 2005 +0200
     6.2 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Thu Sep 15 17:16:56 2005 +0200
     6.3 @@ -725,7 +725,7 @@
     6.4  
     6.5  val emptyset = Symtab.empty
     6.6  
     6.7 -fun singleton v = Symtab.update ((v, ()), emptyset)
     6.8 +fun singleton v = Symtab.update (v, ()) emptyset
     6.9  
    6.10  fun merge a b = Symtab.merge (op =) (a, b)
    6.11  
     7.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Thu Sep 15 17:16:55 2005 +0200
     7.2 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Thu Sep 15 17:16:56 2005 +0200
     7.3 @@ -212,7 +212,7 @@
     7.4      else if (approx_value_term 1 I str) = zero_interval then 
     7.5  	vector
     7.6      else  
     7.7 -	Inttab.curried_update (index, str) vector
     7.8 +	Inttab.update (index, str) vector
     7.9  
    7.10  fun set_vector matrix index vector = 
    7.11      if index < 0 then
    7.12 @@ -220,7 +220,7 @@
    7.13      else if Inttab.is_empty vector then
    7.14  	matrix
    7.15      else
    7.16 -	Inttab.curried_update (index, vector) matrix
    7.17 +	Inttab.update (index, vector) matrix
    7.18  
    7.19  val empty_matrix = Inttab.empty
    7.20  val empty_vector = Inttab.empty
    7.21 @@ -232,9 +232,9 @@
    7.22  fun transpose_matrix matrix = 
    7.23      let
    7.24  	fun upd m j i x =
    7.25 -	    case Inttab.curried_lookup m j of
    7.26 -		SOME v => Inttab.curried_update (j, Inttab.curried_update (i, x) v) m
    7.27 -	      | NONE => Inttab.curried_update (j, Inttab.curried_update (i, x) Inttab.empty) m
    7.28 +	    case Inttab.lookup m j of
    7.29 +		SOME v => Inttab.update (j, Inttab.update (i, x) v) m
    7.30 +	      | NONE => Inttab.update (j, Inttab.update (i, x) Inttab.empty) m
    7.31  
    7.32  	fun updv j (m, (i, s)) = upd m i j s
    7.33  
    7.34 @@ -258,7 +258,7 @@
    7.35  	fun nameof i = 
    7.36  	    let 
    7.37  		val s = "x"^(Int.toString i)
    7.38 -		val _ = change ytable (Inttab.curried_update (i, s))
    7.39 +		val _ = change ytable (Inttab.update (i, s))
    7.40  	    in
    7.41  		s
    7.42  	    end
    7.43 @@ -281,7 +281,7 @@
    7.44  		       		       
    7.45  	fun mk_constr index vector c = 
    7.46  	    let 
    7.47 -		val s = case Inttab.curried_lookup c index of SOME s => s | NONE => "0"
    7.48 +		val s = case Inttab.lookup c index of SOME s => s | NONE => "0"
    7.49  		val (p, s) = split_numstr s
    7.50  		val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
    7.51  	    in
    7.52 @@ -334,7 +334,7 @@
    7.53  		       		       
    7.54  	fun mk_constr index vector c = 
    7.55  	    let 
    7.56 -		val s = case Inttab.curried_lookup c index of SOME s => s | NONE => "0"
    7.57 +		val s = case Inttab.lookup c index of SOME s => s | NONE => "0"
    7.58  		val (p, s) = split_numstr s
    7.59  		val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
    7.60  	    in
    7.61 @@ -358,7 +358,7 @@
    7.62  	val count = ref 0 
    7.63  	fun app (v, (i, s)) = 
    7.64  	    if (!count < size) then
    7.65 -		(count := !count +1 ; Inttab.curried_update (i,s) v)
    7.66 +		(count := !count +1 ; Inttab.update (i,s) v)
    7.67  	    else
    7.68  		v
    7.69      in
    7.70 @@ -368,18 +368,18 @@
    7.71  fun cut_matrix vfilter vsize m = 
    7.72      let 
    7.73  	fun app (m, (i, v)) = 
    7.74 -	    if Inttab.curried_lookup vfilter i = NONE then 
    7.75 +	    if Inttab.lookup vfilter i = NONE then 
    7.76  		m 
    7.77  	    else 
    7.78  		case vsize of
    7.79 -		    NONE => Inttab.curried_update (i,v) m
    7.80 -		  | SOME s => Inttab.curried_update (i, cut_vector s v) m
    7.81 +		    NONE => Inttab.update (i,v) m
    7.82 +		  | SOME s => Inttab.update (i, cut_vector s v) m
    7.83      in
    7.84  	Inttab.foldl app (empty_matrix, m)
    7.85      end
    7.86  		 
    7.87 -fun v_elem_at v i = Inttab.curried_lookup v i
    7.88 -fun m_elem_at m i = Inttab.curried_lookup m i
    7.89 +fun v_elem_at v i = Inttab.lookup v i
    7.90 +fun m_elem_at m i = Inttab.lookup m i
    7.91  
    7.92  fun v_only_elem v = 
    7.93      case Inttab.min_key v of
     8.1 --- a/src/HOL/Matrix/cplex/fspmlp.ML	Thu Sep 15 17:16:55 2005 +0200
     8.2 +++ b/src/HOL/Matrix/cplex/fspmlp.ML	Thu Sep 15 17:16:56 2005 +0200
     8.3 @@ -53,21 +53,21 @@
     8.4  fun add_row_bound g dest_key row_index row_bound = 
     8.5      let 
     8.6  	val x = 
     8.7 -	    case VarGraph.lookup (g, dest_key) of
     8.8 -		NONE => (NONE, Inttab.curried_update (row_index, (row_bound, [])) Inttab.empty)
     8.9 +	    case VarGraph.lookup g dest_key of
    8.10 +		NONE => (NONE, Inttab.update (row_index, (row_bound, [])) Inttab.empty)
    8.11  	      | SOME (sure_bound, f) =>
    8.12  		(sure_bound,
    8.13 -		 case Inttab.curried_lookup f row_index of
    8.14 -		     NONE => Inttab.curried_update (row_index, (row_bound, [])) f
    8.15 +		 case Inttab.lookup f row_index of
    8.16 +		     NONE => Inttab.update (row_index, (row_bound, [])) f
    8.17  		   | SOME _ => raise (Internal "add_row_bound"))				     
    8.18      in
    8.19 -	VarGraph.update ((dest_key, x), g)
    8.20 +	VarGraph.update (dest_key, x) g
    8.21      end    
    8.22  
    8.23  fun update_sure_bound g (key as (_, btype)) bound = 
    8.24      let
    8.25  	val x = 
    8.26 -	    case VarGraph.lookup (g, key) of
    8.27 +	    case VarGraph.lookup g key of
    8.28  		NONE => (SOME bound, Inttab.empty)
    8.29  	      | SOME (NONE, f) => (SOME bound, f)
    8.30  	      | SOME (SOME old_bound, f) => 
    8.31 @@ -76,30 +76,30 @@
    8.32  			  | LOWER => FloatArith.max) 
    8.33  			   old_bound bound), f)
    8.34      in
    8.35 -	VarGraph.update ((key, x), g)
    8.36 +	VarGraph.update (key, x) g
    8.37      end
    8.38  
    8.39  fun get_sure_bound g key = 
    8.40 -    case VarGraph.lookup (g, key) of 
    8.41 +    case VarGraph.lookup g key of 
    8.42  	NONE => NONE
    8.43        | SOME (sure_bound, _) => sure_bound
    8.44  
    8.45  (*fun get_row_bound g key row_index = 
    8.46 -    case VarGraph.lookup (g, key) of
    8.47 +    case VarGraph.lookup g key of
    8.48  	NONE => NONE
    8.49        | SOME (sure_bound, f) =>
    8.50 -	(case Inttab.curried_lookup f row_index of 
    8.51 +	(case Inttab.lookup f row_index of 
    8.52  	     NONE => NONE
    8.53  	   | SOME (row_bound, _) => (sure_bound, row_bound))*)
    8.54      
    8.55  fun add_edge g src_key dest_key row_index coeff = 
    8.56 -    case VarGraph.lookup (g, dest_key) of
    8.57 +    case VarGraph.lookup g dest_key of
    8.58  	NONE => raise (Internal "add_edge: dest_key not found")
    8.59        | SOME (sure_bound, f) =>
    8.60 -	(case Inttab.curried_lookup f row_index of
    8.61 +	(case Inttab.lookup f row_index of
    8.62  	     NONE => raise (Internal "add_edge: row_index not found")
    8.63  	   | SOME (row_bound, sources) => 
    8.64 -	     VarGraph.curried_update (dest_key, (sure_bound, Inttab.curried_update (row_index, (row_bound, (coeff, src_key) :: sources)) f)) g)
    8.65 +	     VarGraph.update (dest_key, (sure_bound, Inttab.update (row_index, (row_bound, (coeff, src_key) :: sources)) f)) g)
    8.66  
    8.67  fun split_graph g = 
    8.68      let
    8.69 @@ -108,8 +108,8 @@
    8.70  		NONE => (r1, r2)
    8.71  	      | SOME bound => 
    8.72  		(case key of
    8.73 -		     (u, UPPER) => (r1, Inttab.curried_update (u, bound) r2)
    8.74 -		   | (u, LOWER) => (Inttab.curried_update (u, bound) r1, r2))
    8.75 +		     (u, UPPER) => (r1, Inttab.update (u, bound) r2)
    8.76 +		   | (u, LOWER) => (Inttab.update (u, bound) r1, r2))
    8.77      in
    8.78  	VarGraph.foldl split ((Inttab.empty, Inttab.empty), g)
    8.79      end
    8.80 @@ -163,7 +163,7 @@
    8.81  					 | LOWER => FloatArith.max old_bound new_bound))				 
    8.82  		    end		
    8.83  	    in
    8.84 -		case VarGraph.lookup (g, key) of
    8.85 +		case VarGraph.lookup g key of
    8.86  		    NONE => NONE
    8.87  		  | SOME (sure_bound, f) =>
    8.88  		    let
    8.89 @@ -195,7 +195,7 @@
    8.90      let
    8.91  	val empty = Inttab.empty
    8.92  
    8.93 -	fun instab t i x = Inttab.curried_update (i, x) t
    8.94 +	fun instab t i x = Inttab.update (i, x) t
    8.95  
    8.96  	fun isnegstr x = String.isPrefix "-" x
    8.97  	fun negstr x = if isnegstr x then String.extract (x, 1, NONE) else "-"^x
    8.98 @@ -280,8 +280,8 @@
    8.99  		let
   8.100  		    val index = xlen-i
   8.101  		    val (r, (r12_1, r12_2)) = abs_estimate (i-1) r1 r2 
   8.102 -		    val b1 = case Inttab.curried_lookup r1 index of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x
   8.103 -		    val b2 = case Inttab.curried_lookup r2 index of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x
   8.104 +		    val b1 = case Inttab.lookup r1 index of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x
   8.105 +		    val b2 = case Inttab.lookup r2 index of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x
   8.106  		    val abs_max = FloatArith.max (FloatArith.neg (FloatArith.negative_part b1)) (FloatArith.positive_part b2)    
   8.107  		in
   8.108  		    (add_row_entry r index abs_max, (add_row_entry r12_1 index b1, add_row_entry r12_2 index b2))
     9.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Sep 15 17:16:55 2005 +0200
     9.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Sep 15 17:16:56 2005 +0200
     9.3 @@ -57,7 +57,7 @@
     9.4  
     9.5  fun axioms_having_consts_aux [] tab thms = thms
     9.6    | axioms_having_consts_aux (c::cs) tab thms =
     9.7 -    let val thms1 = Symtab.curried_lookup tab c
     9.8 +    let val thms1 = Symtab.lookup tab c
     9.9        val thms2 = 
    9.10            case thms1 of (SOME x) => x
    9.11                        | NONE => []
    10.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Sep 15 17:16:55 2005 +0200
    10.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Sep 15 17:16:56 2005 +0200
    10.3 @@ -168,7 +168,7 @@
    10.4  
    10.5          val inject = map (fn r => r RS iffD1)
    10.6            (if i < length newTs then List.nth (constr_inject, i)
    10.7 -            else #inject (the (Symtab.curried_lookup dt_info tname)));
    10.8 +            else #inject (the (Symtab.lookup dt_info tname)));
    10.9  
   10.10          fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
   10.11            let
    11.1 --- a/src/HOL/Tools/datatype_aux.ML	Thu Sep 15 17:16:55 2005 +0200
    11.2 +++ b/src/HOL/Tools/datatype_aux.ML	Thu Sep 15 17:16:56 2005 +0200
    11.3 @@ -299,7 +299,7 @@
    11.4        Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
    11.5  
    11.6      fun get_dt_descr T i tname dts =
    11.7 -      (case Symtab.curried_lookup dt_info tname of
    11.8 +      (case Symtab.lookup dt_info tname of
    11.9           NONE => typ_error T (tname ^ " is not a datatype - can't use it in\
   11.10             \ nested recursion")
   11.11         | (SOME {index, descr, ...}) =>
    12.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Sep 15 17:16:55 2005 +0200
    12.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Sep 15 17:16:56 2005 +0200
    12.3 @@ -281,7 +281,7 @@
    12.4   |  _ => NONE);
    12.5  
    12.6  fun datatype_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
    12.7 -      (case Symtab.curried_lookup (DatatypePackage.get_datatypes thy) s of
    12.8 +      (case Symtab.lookup (DatatypePackage.get_datatypes thy) s of
    12.9           NONE => NONE
   12.10         | SOME {descr, ...} =>
   12.11             if isSome (get_assoc_type thy s) then NONE else
    13.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Sep 15 17:16:55 2005 +0200
    13.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Sep 15 17:16:56 2005 +0200
    13.3 @@ -104,7 +104,7 @@
    13.4  
    13.5  (** theory information about datatypes **)
    13.6  
    13.7 -val datatype_info = Symtab.curried_lookup o get_datatypes;
    13.8 +val datatype_info = Symtab.lookup o get_datatypes;
    13.9  
   13.10  fun datatype_info_err thy name = (case datatype_info thy name of
   13.11        SOME info => info
   13.12 @@ -681,7 +681,7 @@
   13.13        Theory.add_path (space_implode "_" new_type_names) |>
   13.14        add_rules simps case_thms size_thms rec_thms inject distinct
   13.15                  weak_case_congs Simplifier.cong_add_global |> 
   13.16 -      put_datatypes (fold Symtab.curried_update dt_infos dt_info) |>
   13.17 +      put_datatypes (fold Symtab.update dt_infos dt_info) |>
   13.18        add_cases_induct dt_infos induct |>
   13.19        Theory.parent_path |>
   13.20        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
   13.21 @@ -739,7 +739,7 @@
   13.22        Theory.add_path (space_implode "_" new_type_names) |>
   13.23        add_rules simps case_thms size_thms rec_thms inject distinct
   13.24                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
   13.25 -      put_datatypes (fold Symtab.curried_update dt_infos dt_info) |>
   13.26 +      put_datatypes (fold Symtab.update dt_infos dt_info) |>
   13.27        add_cases_induct dt_infos induct |>
   13.28        Theory.parent_path |>
   13.29        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
   13.30 @@ -847,7 +847,7 @@
   13.31        Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
   13.32        add_rules simps case_thms size_thms rec_thms inject distinct
   13.33                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
   13.34 -      put_datatypes (fold Symtab.curried_update dt_infos dt_info) |>
   13.35 +      put_datatypes (fold Symtab.update dt_infos dt_info) |>
   13.36        add_cases_induct dt_infos induction' |>
   13.37        Theory.parent_path |>
   13.38        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    14.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 15 17:16:55 2005 +0200
    14.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 15 17:16:56 2005 +0200
    14.3 @@ -35,7 +35,7 @@
    14.4  
    14.5  
    14.6  fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
    14.7 -  #exhaustion (the (Symtab.curried_lookup dt_info tname));
    14.8 +  #exhaustion (the (Symtab.lookup dt_info tname));
    14.9  
   14.10  (******************************************************************************)
   14.11  
   14.12 @@ -356,7 +356,7 @@
   14.13        let
   14.14          val ks = map fst ds;
   14.15          val (_, (tname, _, _)) = hd ds;
   14.16 -        val {rec_rewrites, rec_names, ...} = the (Symtab.curried_lookup dt_info tname);
   14.17 +        val {rec_rewrites, rec_names, ...} = the (Symtab.lookup dt_info tname);
   14.18  
   14.19          fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) =
   14.20            let
   14.21 @@ -412,7 +412,7 @@
   14.22      fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
   14.23        let
   14.24          val (_, (tname, _, _)) = hd ds;
   14.25 -        val {induction, ...} = the (Symtab.curried_lookup dt_info tname);
   14.26 +        val {induction, ...} = the (Symtab.lookup dt_info tname);
   14.27  
   14.28          fun mk_ind_concl (i, _) =
   14.29            let
    15.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Sep 15 17:16:55 2005 +0200
    15.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Sep 15 17:16:56 2005 +0200
    15.3 @@ -56,7 +56,7 @@
    15.4            let val cs = foldr add_term_consts [] (prems_of thm)
    15.5            in (CodegenData.put
    15.6              {intros = intros |>
    15.7 -             Symtab.curried_update (s, Symtab.curried_lookup_multi intros s @ [(thm, thyname_of s)]),
    15.8 +             Symtab.update (s, Symtab.lookup_multi intros s @ [(thm, thyname_of s)]),
    15.9               graph = foldr (uncurry (Graph.add_edge o pair s))
   15.10                 (Library.foldl add_node (graph, s :: cs)) cs,
   15.11               eqns = eqns} thy, thm)
   15.12 @@ -65,15 +65,15 @@
   15.13      | _ $ (Const ("op =", _) $ t $ _) => (case head_of t of
   15.14          Const (s, _) =>
   15.15            (CodegenData.put {intros = intros, graph = graph,
   15.16 -             eqns = eqns |> Symtab.curried_update
   15.17 -               (s, Symtab.curried_lookup_multi eqns s @ [(thm, thyname_of s)])} thy, thm)
   15.18 +             eqns = eqns |> Symtab.update
   15.19 +               (s, Symtab.lookup_multi eqns s @ [(thm, thyname_of s)])} thy, thm)
   15.20        | _ => (warn thm; p))
   15.21      | _ => (warn thm; p))
   15.22    end;
   15.23  
   15.24  fun get_clauses thy s =
   15.25    let val {intros, graph, ...} = CodegenData.get thy
   15.26 -  in case Symtab.curried_lookup intros s of
   15.27 +  in case Symtab.lookup intros s of
   15.28        NONE => (case InductivePackage.get_inductive thy s of
   15.29          NONE => NONE
   15.30        | SOME ({names, ...}, {intrs, ...}) =>
   15.31 @@ -84,7 +84,7 @@
   15.32            val SOME names = find_first
   15.33              (fn xs => s mem xs) (Graph.strong_conn graph);
   15.34            val intrs = List.concat (map
   15.35 -            (fn s => the (Symtab.curried_lookup intros s)) names);
   15.36 +            (fn s => the (Symtab.lookup intros s)) names);
   15.37            val (_, (_, thyname)) = split_last intrs
   15.38          in SOME (names, thyname, preprocess thy (map fst intrs)) end
   15.39    end;
   15.40 @@ -716,7 +716,7 @@
   15.41             (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
   15.42          handle TERM _ => mk_ind_call thy defs gr dep module t u true)
   15.43    | inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
   15.44 -      (Const (s, _), ts) => (case Symtab.curried_lookup (#eqns (CodegenData.get thy)) s of
   15.45 +      (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of
   15.46          NONE => list_of_indset thy defs gr dep module brack t
   15.47        | SOME eqns =>
   15.48            let
    16.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Sep 15 17:16:55 2005 +0200
    16.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Sep 15 17:16:56 2005 +0200
    16.3 @@ -112,7 +112,7 @@
    16.4  
    16.5  (* get and put data *)
    16.6  
    16.7 -val get_inductive = Symtab.curried_lookup o #1 o InductiveData.get;
    16.8 +val get_inductive = Symtab.lookup o #1 o InductiveData.get;
    16.9  
   16.10  fun the_inductive thy name =
   16.11    (case get_inductive thy name of
   16.12 @@ -123,7 +123,7 @@
   16.13  
   16.14  fun put_inductives names info thy =
   16.15    let
   16.16 -    fun upd ((tab, monos), name) = (Symtab.curried_update_new (name, info) tab, monos);
   16.17 +    fun upd ((tab, monos), name) = (Symtab.update_new (name, info) tab, monos);
   16.18      val tab_monos = Library.foldl upd (InductiveData.get thy, names)
   16.19        handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
   16.20    in InductiveData.put tab_monos thy end;
    17.1 --- a/src/HOL/Tools/primrec_package.ML	Thu Sep 15 17:16:55 2005 +0200
    17.2 +++ b/src/HOL/Tools/primrec_package.ML	Thu Sep 15 17:16:56 2005 +0200
    17.3 @@ -203,7 +203,7 @@
    17.4  
    17.5  fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
    17.6    | find_dts dt_info tnames' (tname::tnames) =
    17.7 -      (case Symtab.curried_lookup dt_info tname of
    17.8 +      (case Symtab.lookup dt_info tname of
    17.9            NONE => primrec_err (quote tname ^ " is not a datatype")
   17.10          | SOME dt =>
   17.11              if tnames' subset (map (#1 o snd) (#descr dt)) then
    18.1 --- a/src/HOL/Tools/recdef_package.ML	Thu Sep 15 17:16:55 2005 +0200
    18.2 +++ b/src/HOL/Tools/recdef_package.ML	Thu Sep 15 17:16:56 2005 +0200
    18.3 @@ -126,12 +126,12 @@
    18.4  val print_recdefs = GlobalRecdefData.print;
    18.5  
    18.6  
    18.7 -val get_recdef = Symtab.curried_lookup o #1 o GlobalRecdefData.get;
    18.8 +val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get;
    18.9  
   18.10  fun put_recdef name info thy =
   18.11    let
   18.12      val (tab, hints) = GlobalRecdefData.get thy;
   18.13 -    val tab' = Symtab.curried_update_new (name, info) tab
   18.14 +    val tab' = Symtab.update_new (name, info) tab
   18.15        handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
   18.16    in GlobalRecdefData.put (tab', hints) thy end;
   18.17  
    19.1 --- a/src/HOL/Tools/recfun_codegen.ML	Thu Sep 15 17:16:55 2005 +0200
    19.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Thu Sep 15 17:16:56 2005 +0200
    19.3 @@ -42,7 +42,7 @@
    19.4      val (s, _) = const_of (prop_of thm);
    19.5    in
    19.6      if Pattern.pattern (lhs_of thm) then
    19.7 -      (CodegenData.put (Symtab.curried_update_multi (s, (thm, optmod)) tab) thy, thm)
    19.8 +      (CodegenData.put (Symtab.update_multi (s, (thm, optmod)) tab) thy, thm)
    19.9      else (warn thm; p)
   19.10    end handle TERM _ => (warn thm; p);
   19.11  
   19.12 @@ -50,9 +50,9 @@
   19.13    let
   19.14      val tab = CodegenData.get thy;
   19.15      val (s, _) = const_of (prop_of thm);
   19.16 -  in case Symtab.curried_lookup tab s of
   19.17 +  in case Symtab.lookup tab s of
   19.18        NONE => p
   19.19 -    | SOME thms => (CodegenData.put (Symtab.curried_update (s,
   19.20 +    | SOME thms => (CodegenData.put (Symtab.update (s,
   19.21          gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy, thm)
   19.22    end handle TERM _ => (warn thm; p);
   19.23  
   19.24 @@ -64,7 +64,7 @@
   19.25      in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
   19.26  
   19.27  fun get_equations thy defs (s, T) =
   19.28 -  (case Symtab.curried_lookup (CodegenData.get thy) s of
   19.29 +  (case Symtab.lookup (CodegenData.get thy) s of
   19.30       NONE => ([], "")
   19.31     | SOME thms => 
   19.32         let val thms' = del_redundant thy []
    20.1 --- a/src/HOL/Tools/record_package.ML	Thu Sep 15 17:16:55 2005 +0200
    20.2 +++ b/src/HOL/Tools/record_package.ML	Thu Sep 15 17:16:56 2005 +0200
    20.3 @@ -301,13 +301,13 @@
    20.4  
    20.5  (* access 'records' *)
    20.6  
    20.7 -val get_record = Symtab.curried_lookup o #records o RecordsData.get;
    20.8 +val get_record = Symtab.lookup o #records o RecordsData.get;
    20.9  
   20.10  fun put_record name info thy =
   20.11    let
   20.12      val {records, sel_upd, equalities, extinjects,extsplit,splits,extfields,fieldext} =
   20.13            RecordsData.get thy;
   20.14 -    val data = make_record_data (Symtab.curried_update (name, info) records)
   20.15 +    val data = make_record_data (Symtab.update (name, info) records)
   20.16        sel_upd equalities extinjects extsplit splits extfields fieldext;
   20.17    in RecordsData.put data thy end;
   20.18  
   20.19 @@ -315,10 +315,10 @@
   20.20  
   20.21  val get_sel_upd = #sel_upd o RecordsData.get;
   20.22  
   20.23 -val get_selectors = Symtab.curried_lookup o #selectors o get_sel_upd;
   20.24 +val get_selectors = Symtab.lookup o #selectors o get_sel_upd;
   20.25  fun is_selector sg name = is_some (get_selectors sg (Sign.intern_const sg name));
   20.26  
   20.27 -val get_updates = Symtab.curried_lookup o #updates o get_sel_upd;
   20.28 +val get_updates = Symtab.lookup o #updates o get_sel_upd;
   20.29  val get_simpset = #simpset o get_sel_upd;
   20.30  
   20.31  fun put_sel_upd names simps thy =
   20.32 @@ -342,11 +342,11 @@
   20.33      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
   20.34            RecordsData.get thy;
   20.35      val data = make_record_data records sel_upd
   20.36 -           (Symtab.curried_update_new (name, thm) equalities) extinjects extsplit
   20.37 +           (Symtab.update_new (name, thm) equalities) extinjects extsplit
   20.38             splits extfields fieldext;
   20.39    in RecordsData.put data thy end;
   20.40  
   20.41 -val get_equalities =Symtab.curried_lookup o #equalities o RecordsData.get;
   20.42 +val get_equalities =Symtab.lookup o #equalities o RecordsData.get;
   20.43  
   20.44  (* access 'extinjects' *)
   20.45  
   20.46 @@ -367,11 +367,11 @@
   20.47      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
   20.48            RecordsData.get thy;
   20.49      val data = make_record_data records sel_upd
   20.50 -      equalities extinjects (Symtab.curried_update_new (name, thm) extsplit) splits
   20.51 +      equalities extinjects (Symtab.update_new (name, thm) extsplit) splits
   20.52        extfields fieldext;
   20.53    in RecordsData.put data thy end;
   20.54  
   20.55 -val get_extsplit = Symtab.curried_lookup o #extsplit o RecordsData.get;
   20.56 +val get_extsplit = Symtab.lookup o #extsplit o RecordsData.get;
   20.57  
   20.58  (* access 'splits' *)
   20.59  
   20.60 @@ -380,17 +380,17 @@
   20.61      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
   20.62            RecordsData.get thy;
   20.63      val data = make_record_data records sel_upd
   20.64 -      equalities extinjects extsplit (Symtab.curried_update_new (name, thmP) splits)
   20.65 +      equalities extinjects extsplit (Symtab.update_new (name, thmP) splits)
   20.66        extfields fieldext;
   20.67    in RecordsData.put data thy end;
   20.68  
   20.69 -val get_splits = Symtab.curried_lookup o #splits o RecordsData.get;
   20.70 +val get_splits = Symtab.lookup o #splits o RecordsData.get;
   20.71  
   20.72  
   20.73  
   20.74  (* extension of a record name *)
   20.75  val get_extension =
   20.76 -  Option.map #extension oo (Symtab.curried_lookup o #records o RecordsData.get);
   20.77 +  Option.map #extension oo (Symtab.lookup o #records o RecordsData.get);
   20.78  
   20.79  
   20.80  (* access 'extfields' *)
   20.81 @@ -401,10 +401,10 @@
   20.82            RecordsData.get thy;
   20.83      val data = make_record_data records sel_upd
   20.84           equalities extinjects extsplit splits
   20.85 -         (Symtab.curried_update_new (name, fields) extfields) fieldext;
   20.86 +         (Symtab.update_new (name, fields) extfields) fieldext;
   20.87    in RecordsData.put data thy end;
   20.88  
   20.89 -val get_extfields = Symtab.curried_lookup o #extfields o RecordsData.get;
   20.90 +val get_extfields = Symtab.lookup o #extfields o RecordsData.get;
   20.91  
   20.92  fun get_extT_fields sg T =
   20.93    let
   20.94 @@ -415,8 +415,8 @@
   20.95      fun varify (a, S) = TVar ((a, midx), S);
   20.96      val varifyT = map_type_tfree varify;
   20.97      val {records,extfields,...} = RecordsData.get sg;
   20.98 -    val (flds,(more,_)) = split_last (Symtab.curried_lookup_multi extfields name);
   20.99 -    val args = map varifyT (snd (#extension (the (Symtab.curried_lookup records recname))));
  20.100 +    val (flds,(more,_)) = split_last (Symtab.lookup_multi extfields name);
  20.101 +    val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
  20.102  
  20.103      val (subst,_) = fold (Sign.typ_unify sg) (but_last args ~~ but_last Ts) (Vartab.empty,0);
  20.104      val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds;
  20.105 @@ -438,13 +438,13 @@
  20.106      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
  20.107             RecordsData.get thy;
  20.108      val fieldext' =
  20.109 -      fold (fn field => Symtab.curried_update_new (field, extname_types)) fields fieldext;
  20.110 +      fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
  20.111      val data=make_record_data records sel_upd equalities extinjects extsplit
  20.112                splits extfields fieldext';
  20.113    in RecordsData.put data thy end;
  20.114  
  20.115  
  20.116 -val get_fieldext = Symtab.curried_lookup o #fieldext o RecordsData.get;
  20.117 +val get_fieldext = Symtab.lookup o #fieldext o RecordsData.get;
  20.118  
  20.119  (* parent records *)
  20.120  
  20.121 @@ -819,7 +819,7 @@
  20.122    let
  20.123      val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg;
  20.124      val extsplits =
  20.125 -            Library.foldl (fn (thms,(n,_)) => the_list (Symtab.curried_lookup extsplit n) @ thms)
  20.126 +            Library.foldl (fn (thms,(n,_)) => the_list (Symtab.lookup extsplit n) @ thms)
  20.127                      ([],dest_recTs T);
  20.128      val thms = (case get_splits sg (rec_id (~1) T) of
  20.129                     SOME (all_thm,_,_,_) =>
  20.130 @@ -835,7 +835,7 @@
  20.131  local
  20.132  fun eq (s1:string) (s2:string) = (s1 = s2);
  20.133  fun has_field extfields f T =
  20.134 -     exists (fn (eN,_) => exists (eq f o fst) (Symtab.curried_lookup_multi extfields eN))
  20.135 +     exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_multi extfields eN))
  20.136         (dest_recTs T);
  20.137  in
  20.138  (* record_simproc *)
  20.139 @@ -861,7 +861,7 @@
  20.140                val {sel_upd={updates,...},extfields,...} = RecordsData.get sg;
  20.141  
  20.142                fun mk_eq_terms ((upd as Const (u,Type(_,[kT,_]))) $ k $ r) =
  20.143 -                  (case Symtab.curried_lookup updates u of
  20.144 +                  (case Symtab.lookup updates u of
  20.145                       NONE => NONE
  20.146                     | SOME u_name
  20.147                       => if u_name = s
    21.1 --- a/src/HOL/Tools/refute.ML	Thu Sep 15 17:16:55 2005 +0200
    21.2 +++ b/src/HOL/Tools/refute.ML	Thu Sep 15 17:16:56 2005 +0200
    21.3 @@ -298,11 +298,11 @@
    21.4  	let
    21.5  		val {interpreters, printers, parameters} = RefuteData.get thy
    21.6  	in
    21.7 -		case Symtab.curried_lookup parameters name of
    21.8 +		case Symtab.lookup parameters name of
    21.9  		  NONE   => RefuteData.put
   21.10  			{interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy
   21.11  		| SOME _ => RefuteData.put
   21.12 -			{interpreters = interpreters, printers = printers, parameters = Symtab.curried_update (name, value) parameters} thy
   21.13 +			{interpreters = interpreters, printers = printers, parameters = Symtab.update (name, value) parameters} thy
   21.14  	end;
   21.15  
   21.16  (* ------------------------------------------------------------------------- *)
   21.17 @@ -312,7 +312,7 @@
   21.18  
   21.19  	(* theory -> string -> string option *)
   21.20  
   21.21 -	val get_default_param = Symtab.curried_lookup o #parameters o RefuteData.get;
   21.22 +	val get_default_param = Symtab.lookup o #parameters o RefuteData.get;
   21.23  
   21.24  (* ------------------------------------------------------------------------- *)
   21.25  (* get_default_params: returns a list of all '(name, value)' pairs that are  *)
    22.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Sep 15 17:16:55 2005 +0200
    22.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Sep 15 17:16:56 2005 +0200
    22.3 @@ -261,7 +261,7 @@
    22.4  (*Populate the clause cache using the supplied theorems*)
    22.5  fun skolemlist [] thy = thy
    22.6    | skolemlist ((name,th)::nths) thy = 
    22.7 -      (case Symtab.curried_lookup (!clause_cache) name of
    22.8 +      (case Symtab.lookup (!clause_cache) name of
    22.9  	  NONE => 
   22.10  	    let val (nnfth,ok) = (to_nnf thy th, true)  
   22.11  	                 handle THM _ => (asm_rl, false)
   22.12 @@ -269,7 +269,7 @@
   22.13                  if ok then
   22.14                      let val (skoths,thy') = skolem thy (name, nnfth)
   22.15  			val cls = Meson.make_cnf skoths nnfth
   22.16 -		    in change clause_cache (Symtab.curried_update (name, (th, cls)));
   22.17 +		    in change clause_cache (Symtab.update (name, (th, cls)));
   22.18  			skolemlist nths thy'
   22.19  		    end
   22.20  		else skolemlist nths thy
   22.21 @@ -280,15 +280,15 @@
   22.22  fun cnf_axiom (name,th) =
   22.23      case name of
   22.24  	  "" => cnf_axiom_aux th (*no name, so can't cache*)
   22.25 -	| s  => case Symtab.curried_lookup (!clause_cache) s of
   22.26 +	| s  => case Symtab.lookup (!clause_cache) s of
   22.27  	  	  NONE => 
   22.28  		    let val cls = cnf_axiom_aux th
   22.29 -		    in change clause_cache (Symtab.curried_update (s, (th, cls))); cls end
   22.30 +		    in change clause_cache (Symtab.update (s, (th, cls))); cls end
   22.31  	        | SOME(th',cls) =>
   22.32  		    if eq_thm(th,th') then cls
   22.33  		    else (*New theorem stored under the same name? Possible??*)
   22.34  		      let val cls = cnf_axiom_aux th
   22.35 -		      in change clause_cache (Symtab.curried_update (s, (th, cls))); cls end;
   22.36 +		      in change clause_cache (Symtab.update (s, (th, cls))); cls end;
   22.37  
   22.38  fun pairname th = (Thm.name_of_thm th, th);
   22.39  
    23.1 --- a/src/HOL/Tools/res_clause.ML	Thu Sep 15 17:16:55 2005 +0200
    23.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Sep 15 17:16:56 2005 +0200
    23.3 @@ -141,12 +141,12 @@
    23.4  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
    23.5  
    23.6  fun make_fixed_const c =
    23.7 -    case Symtab.curried_lookup const_trans_table c of
    23.8 +    case Symtab.lookup const_trans_table c of
    23.9          SOME c' => c'
   23.10        | NONE =>  const_prefix ^ ascii_of c;
   23.11  
   23.12  fun make_fixed_type_const c = 
   23.13 -    case Symtab.curried_lookup type_const_trans_table c of
   23.14 +    case Symtab.lookup type_const_trans_table c of
   23.15          SOME c' => c'
   23.16        | NONE =>  tconst_prefix ^ ascii_of c;
   23.17  
    24.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Sep 15 17:16:55 2005 +0200
    24.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Sep 15 17:16:56 2005 +0200
    24.3 @@ -62,7 +62,7 @@
    24.4  end);
    24.5  
    24.6  fun put_typedef newT oldT Abs_name Rep_name =
    24.7 -  TypedefData.map (Symtab.curried_update_new (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)));
    24.8 +  TypedefData.map (Symtab.update_new (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)));
    24.9  
   24.10  
   24.11  
   24.12 @@ -299,7 +299,7 @@
   24.13          val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
   24.14        in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
   24.15      fun lookup f T =
   24.16 -      (case Symtab.curried_lookup (TypedefData.get thy) (get_name T) of
   24.17 +      (case Symtab.lookup (TypedefData.get thy) (get_name T) of
   24.18          NONE => ""
   24.19        | SOME s => f s);
   24.20    in
   24.21 @@ -320,7 +320,7 @@
   24.22    | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
   24.23  
   24.24  fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
   24.25 -      (case Symtab.curried_lookup (TypedefData.get thy) s of
   24.26 +      (case Symtab.lookup (TypedefData.get thy) s of
   24.27           NONE => NONE
   24.28         | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
   24.29             if is_some (Codegen.get_assoc_type thy tname) then NONE else
    25.1 --- a/src/Provers/Arith/cancel_numerals.ML	Thu Sep 15 17:16:55 2005 +0200
    25.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Thu Sep 15 17:16:56 2005 +0200
    25.3 @@ -54,7 +54,7 @@
    25.4  
    25.5  (*For t = #n*u then put u in the table*)
    25.6  fun update_by_coeff t =
    25.7 -  Termtab.curried_update (#2 (Data.dest_coeff t), ());
    25.8 +  Termtab.update (#2 (Data.dest_coeff t), ());
    25.9  
   25.10  (*a left-to-right scan of terms1, seeking a term of the form #n*u, where
   25.11    #m*u is in terms2 for some m*)
    26.1 --- a/src/Provers/Arith/combine_numerals.ML	Thu Sep 15 17:16:55 2005 +0200
    26.2 +++ b/src/Provers/Arith/combine_numerals.ML	Thu Sep 15 17:16:56 2005 +0200
    26.3 @@ -57,9 +57,9 @@
    26.4    | find_repeated (tab, past, t::terms) =
    26.5        case try Data.dest_coeff t of
    26.6  	  SOME(n,u) => 
    26.7 -	      (case Termtab.curried_lookup tab u of
    26.8 +	      (case Termtab.lookup tab u of
    26.9  		  SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
   26.10 -		| NONE => find_repeated (Termtab.curried_update (u, n) tab, 
   26.11 +		| NONE => find_repeated (Termtab.update (u, n) tab, 
   26.12  					 t::past,  terms))
   26.13  	| NONE => find_repeated (tab, t::past, terms);
   26.14  
    27.1 --- a/src/Provers/Arith/extract_common_term.ML	Thu Sep 15 17:16:55 2005 +0200
    27.2 +++ b/src/Provers/Arith/extract_common_term.ML	Thu Sep 15 17:16:56 2005 +0200
    27.3 @@ -39,7 +39,7 @@
    27.4  
    27.5  (*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
    27.6  fun find_common (terms1,terms2) =
    27.7 -  let val tab2 = fold (Termtab.curried_update o rpair ()) terms2 Termtab.empty
    27.8 +  let val tab2 = fold (Termtab.update o rpair ()) terms2 Termtab.empty
    27.9        fun seek [] = raise TERM("find_common", []) 
   27.10  	| seek (u::terms) =
   27.11  	      if Termtab.defined tab2 u then u
    28.1 --- a/src/Pure/General/graph.ML	Thu Sep 15 17:16:55 2005 +0200
    28.2 +++ b/src/Pure/General/graph.ML	Thu Sep 15 17:16:56 2005 +0200
    28.3 @@ -86,11 +86,11 @@
    28.4  fun maximals (Graph tab) = Table.fold (fn (m, (_, (_, []))) => cons m | _ => I) tab [];
    28.5  
    28.6  fun get_entry (Graph tab) x =
    28.7 -  (case Table.curried_lookup tab x of
    28.8 +  (case Table.lookup tab x of
    28.9      SOME entry => entry
   28.10    | NONE => raise UNDEF x);
   28.11  
   28.12 -fun map_entry x f (G as Graph tab) = Graph (Table.curried_update (x, f (get_entry G x)) tab);
   28.13 +fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab);
   28.14  
   28.15  
   28.16  (* nodes *)
   28.17 @@ -142,7 +142,7 @@
   28.18  (* nodes *)
   28.19  
   28.20  fun new_node (x, info) (Graph tab) =
   28.21 -  Graph (Table.curried_update_new (x, (info, ([], []))) tab);
   28.22 +  Graph (Table.update_new (x, (info, ([], []))) tab);
   28.23  
   28.24  fun default_node (x, info) (Graph tab) =
   28.25    Graph (Table.default (x, (info, ([], []))) tab);
    29.1 --- a/src/Pure/General/name_space.ML	Thu Sep 15 17:16:55 2005 +0200
    29.2 +++ b/src/Pure/General/name_space.ML	Thu Sep 15 17:16:56 2005 +0200
    29.3 @@ -113,7 +113,7 @@
    29.4  val empty = NameSpace Symtab.empty;
    29.5  
    29.6  fun lookup (NameSpace tab) xname =
    29.7 -  (case Symtab.curried_lookup tab xname of
    29.8 +  (case Symtab.lookup tab xname of
    29.9      NONE => (xname, true)
   29.10    | SOME ([], []) => (xname, true)
   29.11    | SOME ([name], _) => (name, true)
   29.12 @@ -150,7 +150,7 @@
   29.13  (* basic operations *)
   29.14  
   29.15  fun map_space f xname (NameSpace tab) =
   29.16 -  NameSpace (Symtab.curried_update (xname, f (if_none (Symtab.curried_lookup tab xname) ([], []))) tab);
   29.17 +  NameSpace (Symtab.update (xname, f (if_none (Symtab.lookup tab xname) ([], []))) tab);
   29.18  
   29.19  fun del (name: string) = remove (op =) name;
   29.20  fun add name names = name :: del name names;
    30.1 --- a/src/Pure/General/output.ML	Thu Sep 15 17:16:55 2005 +0200
    30.2 +++ b/src/Pure/General/output.ML	Thu Sep 15 17:16:56 2005 +0200
    30.3 @@ -84,7 +84,7 @@
    30.4  
    30.5  exception MISSING_DEFAULT_OUTPUT;
    30.6  
    30.7 -fun lookup_mode name = Symtab.curried_lookup (! modes) name;
    30.8 +fun lookup_mode name = Symtab.lookup (! modes) name;
    30.9  
   30.10  fun get_mode () =
   30.11    (case Library.get_first lookup_mode (! print_mode) of SOME p => p
   30.12 @@ -141,7 +141,7 @@
   30.13  fun add_mode name (f, g, h) =
   30.14   (if is_none (lookup_mode name) then ()
   30.15    else warning ("Redeclaration of symbol print mode: " ^ quote name);
   30.16 -  modes := Symtab.curried_update (name, {output_width = f, indent = g, raw = h}) (! modes));
   30.17 +  modes := Symtab.update (name, {output_width = f, indent = g, raw = h}) (! modes));
   30.18  
   30.19  
   30.20  (* produce errors *)
    31.1 --- a/src/Pure/General/symbol.ML	Thu Sep 15 17:16:55 2005 +0200
    31.2 +++ b/src/Pure/General/symbol.ML	Thu Sep 15 17:16:56 2005 +0200
    31.3 @@ -350,7 +350,7 @@
    31.4      else if is_ascii_quasi s then Quasi
    31.5      else if is_ascii_blank s then Blank
    31.6      else if is_char s then Other
    31.7 -    else if_none (Symtab.curried_lookup symbol_kinds s) Other;
    31.8 +    else if_none (Symtab.lookup symbol_kinds s) Other;
    31.9  end;
   31.10  
   31.11  fun is_letter s = kind s = Letter;
    32.1 --- a/src/Pure/General/table.ML	Thu Sep 15 17:16:55 2005 +0200
    32.2 +++ b/src/Pure/General/table.ML	Thu Sep 15 17:16:56 2005 +0200
    32.3 @@ -32,12 +32,9 @@
    32.4    val exists: (key * 'a -> bool) -> 'a table -> bool
    32.5    val forall: (key * 'a -> bool) -> 'a table -> bool
    32.6    val defined: 'a table -> key -> bool
    32.7 -  val lookup: 'a table * key -> 'a option
    32.8 -  val update: (key * 'a) * 'a table -> 'a table
    32.9 -  val update_new: (key * 'a) * 'a table -> 'a table                    (*exception DUP*)
   32.10 -  val curried_lookup: 'a table -> key -> 'a option
   32.11 -  val curried_update: (key * 'a) -> 'a table -> 'a table
   32.12 -  val curried_update_new: (key * 'a) -> 'a table -> 'a table           (*exception DUP*)
   32.13 +  val lookup: 'a table -> key -> 'a option
   32.14 +  val update: (key * 'a) -> 'a table -> 'a table
   32.15 +  val update_new: (key * 'a) -> 'a table -> 'a table                   (*exception DUP*)
   32.16    val default: key * 'a -> 'a table -> 'a table
   32.17    val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
   32.18    val make: (key * 'a) list -> 'a table                                (*exception DUPS*)
   32.19 @@ -50,10 +47,8 @@
   32.20    val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool
   32.21    val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table    (*exception DUP*)
   32.22    val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
   32.23 -  val lookup_multi: 'a list table * key -> 'a list
   32.24 -  val update_multi: (key * 'a) * 'a list table -> 'a list table
   32.25 -  val curried_lookup_multi: 'a list table -> key -> 'a list
   32.26 -  val curried_update_multi: (key * 'a) -> 'a list table -> 'a list table
   32.27 +  val lookup_multi: 'a list table -> key -> 'a list
   32.28 +  val update_multi: (key * 'a) -> 'a list table -> 'a list table
   32.29    val remove_multi: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
   32.30    val make_multi: (key * 'a) list -> 'a list table
   32.31    val dest_multi: 'a list table -> (key * 'a) list
   32.32 @@ -136,25 +131,23 @@
   32.33  
   32.34  (* lookup *)
   32.35  
   32.36 -fun curried_lookup Empty _ = NONE
   32.37 -  | curried_lookup (Branch2 (left, (k, x), right)) key =
   32.38 +fun lookup Empty _ = NONE
   32.39 +  | lookup (Branch2 (left, (k, x), right)) key =
   32.40        (case Key.ord (key, k) of
   32.41 -        LESS => curried_lookup left key
   32.42 +        LESS => lookup left key
   32.43        | EQUAL => SOME x
   32.44 -      | GREATER => curried_lookup right key)
   32.45 -  | curried_lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right)) key =
   32.46 +      | GREATER => lookup right key)
   32.47 +  | lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right)) key =
   32.48        (case Key.ord (key, k1) of
   32.49 -        LESS => curried_lookup left key
   32.50 +        LESS => lookup left key
   32.51        | EQUAL => SOME x1
   32.52        | GREATER =>
   32.53            (case Key.ord (key, k2) of
   32.54 -            LESS => curried_lookup mid key
   32.55 +            LESS => lookup mid key
   32.56            | EQUAL => SOME x2
   32.57 -          | GREATER => curried_lookup right key));
   32.58 +          | GREATER => lookup right key));
   32.59  
   32.60 -fun lookup (tab, key) = curried_lookup tab key;
   32.61 -
   32.62 -fun defined tab key = is_some (curried_lookup tab key);
   32.63 +fun defined tab key = is_some (lookup tab key);
   32.64  
   32.65  
   32.66  (* updates *)
   32.67 @@ -209,11 +202,9 @@
   32.68      handle SAME => tab
   32.69    end;
   32.70  
   32.71 -fun update ((key, x), tab) = modify key (fn _ => x) tab;
   32.72 -fun update_new ((key, x), tab) = modify key (fn NONE => x | SOME _ => raise DUP key) tab;
   32.73 -fun curried_update (key, x) tab = modify key (fn _ => x) tab;
   32.74 -fun curried_update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab;
   32.75 -fun default (p as (key, x)) tab = if defined tab key then tab else curried_update p tab;
   32.76 +fun update (key, x) tab = modify key (fn _ => x) tab;
   32.77 +fun update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab;
   32.78 +fun default (p as (key, x)) tab = if defined tab key then tab else update p tab;
   32.79  fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x);
   32.80  
   32.81  
   32.82 @@ -223,7 +214,7 @@
   32.83    let
   32.84      fun add (key, x) (tab, dups) =
   32.85        if defined tab key then (tab, key :: dups)
   32.86 -      else (curried_update (key, x) tab, dups);
   32.87 +      else (update (key, x) tab, dups);
   32.88    in
   32.89      (case fold add args (table, []) of
   32.90        (table', []) => table'
   32.91 @@ -319,7 +310,7 @@
   32.92  (* member, insert and remove *)
   32.93  
   32.94  fun member eq tab (key, x) =
   32.95 -  (case curried_lookup tab key of
   32.96 +  (case lookup tab key of
   32.97      NONE => false
   32.98    | SOME y => eq (x, y));
   32.99  
  32.100 @@ -327,7 +318,7 @@
  32.101    modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else raise DUP key);
  32.102  
  32.103  fun remove eq (key, x) tab =
  32.104 -  (case curried_lookup tab key of
  32.105 +  (case lookup tab key of
  32.106      NONE => tab
  32.107    | SOME y => if eq (x, y) then delete key tab else tab);
  32.108  
  32.109 @@ -337,11 +328,11 @@
  32.110  fun join f (table1, table2) =
  32.111    let
  32.112      fun add (key, x) (tab, dups) =
  32.113 -      (case curried_lookup tab key of
  32.114 -        NONE => (curried_update (key, x) tab, dups)
  32.115 +      (case lookup tab key of
  32.116 +        NONE => (update (key, x) tab, dups)
  32.117        | SOME y =>
  32.118            (case f key (y, x) of
  32.119 -            SOME z => (curried_update (key, z) tab, dups)
  32.120 +            SOME z => (update (key, z) tab, dups)
  32.121            | NONE => (tab, key :: dups)));
  32.122    in
  32.123      (case fold_table add table2 (table1, []) of
  32.124 @@ -354,17 +345,14 @@
  32.125  
  32.126  (* tables with multiple entries per key *)
  32.127  
  32.128 -fun lookup_multi arg = if_none (lookup arg) [];
  32.129 -fun update_multi ((key, x), tab) = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;
  32.130 -
  32.131 -fun curried_lookup_multi tab key = if_none (curried_lookup tab key) [];
  32.132 -fun curried_update_multi (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;
  32.133 +fun lookup_multi tab key = if_none (lookup tab key) [];
  32.134 +fun update_multi (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;
  32.135  
  32.136  fun remove_multi eq (key, x) tab =
  32.137    map_entry key (fn xs => (case Library.remove eq x xs of [] => raise UNDEF key | ys => ys)) tab
  32.138    handle UNDEF _ => delete key tab;
  32.139  
  32.140 -fun make_multi args = fold_rev curried_update_multi args empty;
  32.141 +fun make_multi args = fold_rev update_multi args empty;
  32.142  fun dest_multi tab = List.concat (map (fn (key, xs) => map (pair key) xs) (dest tab));
  32.143  fun merge_multi eq = join (fn _ => fn (xs, xs') => SOME (gen_merge_lists eq xs xs'));
  32.144  fun merge_multi' eq = join (fn _ => fn (xs, xs') => SOME (gen_merge_lists' eq xs xs'));
    33.1 --- a/src/Pure/IsaPlanner/term_lib.ML	Thu Sep 15 17:16:55 2005 +0200
    33.2 +++ b/src/Pure/IsaPlanner/term_lib.ML	Thu Sep 15 17:16:56 2005 +0200
    33.3 @@ -516,10 +516,10 @@
    33.4  (* a runtime-quick function which makes sure that every variable has a
    33.5  unique name *)
    33.6  fun unique_namify_aux (ntab,(Abs(s,ty,t))) =
    33.7 -    (case Symtab.curried_lookup ntab s of
    33.8 +    (case Symtab.lookup ntab s of
    33.9         NONE =>
   33.10         let
   33.11 -	 val (ntab2,t2) = unique_namify_aux (Symtab.curried_update (s, s) ntab, t)
   33.12 +	 val (ntab2,t2) = unique_namify_aux (Symtab.update (s, s) ntab, t)
   33.13         in
   33.14  	 (ntab2,Abs(s,ty,t2))
   33.15         end
   33.16 @@ -527,7 +527,7 @@
   33.17         let
   33.18  	 val s_new = (Term.variant (Symtab.keys ntab) s)
   33.19  	 val (ntab2,t2) =
   33.20 -	     unique_namify_aux (Symtab.curried_update (s_new, s_new) ntab, t)
   33.21 +	     unique_namify_aux (Symtab.update (s_new, s_new) ntab, t)
   33.22         in
   33.23  	 (ntab2,Abs(s_new,ty,t2))
   33.24         end)
   33.25 @@ -540,12 +540,12 @@
   33.26      end
   33.27    | unique_namify_aux (nt as (ntab,Const x)) = nt
   33.28    | unique_namify_aux (nt as (ntab,f as Free (s,ty))) =
   33.29 -    (case Symtab.curried_lookup ntab s of
   33.30 -       NONE => (Symtab.curried_update (s, s) ntab, f)
   33.31 +    (case Symtab.lookup ntab s of
   33.32 +       NONE => (Symtab.update (s, s) ntab, f)
   33.33       | SOME _ => nt)
   33.34    | unique_namify_aux (nt as (ntab,v as Var ((s,i),ty))) =
   33.35 -    (case Symtab.curried_lookup ntab s of
   33.36 -       NONE => (Symtab.curried_update (s, s) ntab, v)
   33.37 +    (case Symtab.lookup ntab s of
   33.38 +       NONE => (Symtab.update (s, s) ntab, v)
   33.39       | SOME _ => nt)
   33.40    | unique_namify_aux (nt as (ntab, Bound i)) = nt;
   33.41  		
   33.42 @@ -559,11 +559,11 @@
   33.43  sematics of the term. This is really a trick for our embedding code. *)
   33.44  
   33.45  fun bounds_to_frees_aux T (ntab,(Abs(s,ty,t))) =
   33.46 -    (case Symtab.curried_lookup ntab s of
   33.47 +    (case Symtab.lookup ntab s of
   33.48        NONE =>
   33.49        let
   33.50  	val (ntab2,t2) =
   33.51 -          bounds_to_frees_aux ((s,ty)::T) (Symtab.curried_update (s, s) ntab, t)
   33.52 +          bounds_to_frees_aux ((s,ty)::T) (Symtab.update (s, s) ntab, t)
   33.53        in
   33.54  	(ntab2,Abs(s,ty,t2))
   33.55        end
   33.56 @@ -572,7 +572,7 @@
   33.57  	val s_new = (Term.variant (Symtab.keys ntab) s)
   33.58  	val (ntab2,t2) =
   33.59  	  bounds_to_frees_aux ((s_new,ty)::T)
   33.60 -            (Symtab.curried_update (s_new, s_new) ntab, t)
   33.61 +            (Symtab.update (s_new, s_new) ntab, t)
   33.62        in
   33.63  	(ntab2,Abs(s_new,ty,t2))
   33.64        end)
   33.65 @@ -585,12 +585,12 @@
   33.66      end
   33.67    | bounds_to_frees_aux T (nt as (ntab,Const x)) = nt
   33.68    | bounds_to_frees_aux T (nt as (ntab,f as Free (s,ty))) =
   33.69 -    (case Symtab.curried_lookup ntab s of
   33.70 -      NONE => (Symtab.curried_update (s, s) ntab, f)
   33.71 +    (case Symtab.lookup ntab s of
   33.72 +      NONE => (Symtab.update (s, s) ntab, f)
   33.73      | SOME _ => nt)
   33.74    | bounds_to_frees_aux T (nt as (ntab,v as Var ((s,i),ty))) =
   33.75 -     (case Symtab.curried_lookup ntab s of
   33.76 -      NONE => (Symtab.curried_update (s, s) ntab, v)
   33.77 +     (case Symtab.lookup ntab s of
   33.78 +      NONE => (Symtab.update (s, s) ntab, v)
   33.79      | SOME _ => nt)
   33.80    | bounds_to_frees_aux T (nt as (ntab, Bound i)) =
   33.81      let
    34.1 --- a/src/Pure/Isar/attrib.ML	Thu Sep 15 17:16:55 2005 +0200
    34.2 +++ b/src/Pure/Isar/attrib.ML	Thu Sep 15 17:16:56 2005 +0200
    34.3 @@ -104,7 +104,7 @@
    34.4      val attrs = #2 (AttributesData.get thy);
    34.5      fun attr src =
    34.6        let val ((name, _), pos) = Args.dest_src src in
    34.7 -        (case Symtab.curried_lookup attrs name of
    34.8 +        (case Symtab.lookup attrs name of
    34.9            NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
   34.10          | SOME ((p, _), _) => transform_failure (curry ATTRIB_FAIL (name, pos)) (which p src))
   34.11        end;
    35.1 --- a/src/Pure/Isar/isar_output.ML	Thu Sep 15 17:16:55 2005 +0200
    35.2 +++ b/src/Pure/Isar/isar_output.ML	Thu Sep 15 17:16:56 2005 +0200
    35.3 @@ -59,7 +59,7 @@
    35.4  fun add_item kind (name, x) tab =
    35.5   (if not (Symtab.defined tab name) then ()
    35.6    else warning ("Redefined antiquotation " ^ kind ^ ": " ^ quote name);
    35.7 -  Symtab.curried_update (name, x) tab);
    35.8 +  Symtab.update (name, x) tab);
    35.9  
   35.10  in
   35.11  
   35.12 @@ -68,13 +68,13 @@
   35.13  
   35.14  fun command src =
   35.15    let val ((name, _), pos) = Args.dest_src src in
   35.16 -    (case Symtab.curried_lookup (! global_commands) name of
   35.17 +    (case Symtab.lookup (! global_commands) name of
   35.18        NONE => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos)
   35.19      | SOME f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src))
   35.20    end;
   35.21  
   35.22  fun option (name, s) f () =
   35.23 -  (case Symtab.curried_lookup (! global_options) name of
   35.24 +  (case Symtab.lookup (! global_options) name of
   35.25      NONE => error ("Unknown antiquotation option: " ^ quote name)
   35.26    | SOME opt => opt s f ());
   35.27  
    36.1 --- a/src/Pure/Isar/locale.ML	Thu Sep 15 17:16:55 2005 +0200
    36.2 +++ b/src/Pure/Isar/locale.ML	Thu Sep 15 17:16:56 2005 +0200
    36.3 @@ -182,7 +182,7 @@
    36.4  fun tinst_tab_type tinst T = if Symtab.is_empty tinst
    36.5        then T
    36.6        else Term.map_type_tfree
    36.7 -        (fn (v as (x, _)) => getOpt (Symtab.curried_lookup tinst x, (TFree v))) T;
    36.8 +        (fn (v as (x, _)) => getOpt (Symtab.lookup tinst x, (TFree v))) T;
    36.9  
   36.10  fun tinst_tab_term tinst t = if Symtab.is_empty tinst
   36.11        then t
   36.12 @@ -215,7 +215,7 @@
   36.13        else (* instantiate terms and types simultaneously *)
   36.14          let
   36.15            fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T)
   36.16 -            | instf (Free (x, T)) = (case Symtab.curried_lookup inst x of
   36.17 +            | instf (Free (x, T)) = (case Symtab.lookup inst x of
   36.18                   NONE => Free (x, tinst_tab_type tinst T)
   36.19                 | SOME t => t)
   36.20              | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T)
   36.21 @@ -336,7 +336,7 @@
   36.22                  val sups =
   36.23                    List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs);
   36.24                  val sups' = map (apfst untermify) sups
   36.25 -              in (Termtab.curried_update (t, (attn, [])) regs, sups') end
   36.26 +              in (Termtab.update (t, (attn, [])) regs, sups') end
   36.27        | _ => (regs, []))
   36.28      end;
   36.29  
   36.30 @@ -345,9 +345,9 @@
   36.31    fun add_witness ts thm regs =
   36.32      let
   36.33        val t = termify ts;
   36.34 -      val (x, thms) = valOf (Termtab.curried_lookup regs t);
   36.35 +      val (x, thms) = valOf (Termtab.lookup regs t);
   36.36      in
   36.37 -      Termtab.curried_update (t, (x, thm::thms)) regs
   36.38 +      Termtab.update (t, (x, thm::thms)) regs
   36.39      end;
   36.40  end;
   36.41  
   36.42 @@ -412,9 +412,9 @@
   36.43  
   36.44  fun put_locale name loc =
   36.45    GlobalLocalesData.map (fn (space, locs, regs) =>
   36.46 -    (space, Symtab.curried_update (name, loc) locs, regs));
   36.47 -
   36.48 -fun get_locale thy name = Symtab.curried_lookup (#2 (GlobalLocalesData.get thy)) name;
   36.49 +    (space, Symtab.update (name, loc) locs, regs));
   36.50 +
   36.51 +fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name;
   36.52  
   36.53  fun the_locale thy name =
   36.54    (case get_locale thy name of
   36.55 @@ -431,7 +431,7 @@
   36.56  (* retrieve registration from theory or context *)
   36.57  
   36.58  fun gen_get_registrations get thy_ctxt name =
   36.59 -  case Symtab.curried_lookup (get thy_ctxt) name of
   36.60 +  case Symtab.lookup (get thy_ctxt) name of
   36.61        NONE => []
   36.62      | SOME reg => Registrations.dest reg;
   36.63  
   36.64 @@ -441,7 +441,7 @@
   36.65       gen_get_registrations LocalLocalesData.get;
   36.66  
   36.67  fun gen_get_registration get thy_of thy_ctxt (name, ps) =
   36.68 -  case Symtab.curried_lookup (get thy_ctxt) name of
   36.69 +  case Symtab.lookup (get thy_ctxt) name of
   36.70        NONE => NONE
   36.71      | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
   36.72  
   36.73 @@ -466,7 +466,7 @@
   36.74    map_data (fn regs =>
   36.75      let
   36.76        val thy = thy_of thy_ctxt;
   36.77 -      val reg = getOpt (Symtab.curried_lookup regs name, Registrations.empty);
   36.78 +      val reg = getOpt (Symtab.lookup regs name, Registrations.empty);
   36.79        val (reg', sups) = Registrations.insert thy (ps, attn) reg;
   36.80        val _ = if not (null sups) then warning
   36.81                  ("Subsumed interpretation(s) of locale " ^
   36.82 @@ -474,7 +474,7 @@
   36.83                   "\nby interpretation(s) with the following prefix(es):\n" ^
   36.84                    commas_quote (map (fn (_, ((s, _), _)) => s) sups))
   36.85                else ();
   36.86 -    in Symtab.curried_update (name, reg') regs end) thy_ctxt;
   36.87 +    in Symtab.update (name, reg') regs end) thy_ctxt;
   36.88  
   36.89  val put_global_registration =
   36.90       gen_put_registration (fn f =>
   36.91 @@ -559,7 +559,7 @@
   36.92  
   36.93      val loc_int = intern thy loc;
   36.94      val regs = get_regs thy_ctxt;
   36.95 -    val loc_regs = Symtab.curried_lookup regs loc_int;
   36.96 +    val loc_regs = Symtab.lookup regs loc_int;
   36.97    in
   36.98      (case loc_regs of
   36.99          NONE => Pretty.str ("no interpretations in " ^ msg)
  36.100 @@ -771,7 +771,7 @@
  36.101  fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss));
  36.102  fun params_syn_of syn elemss =
  36.103    gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |>
  36.104 -    map (apfst (fn x => (x, valOf (Symtab.curried_lookup syn x))));
  36.105 +    map (apfst (fn x => (x, valOf (Symtab.lookup syn x))));
  36.106  
  36.107  
  36.108  (* CB: param_types has the following type:
  36.109 @@ -1017,7 +1017,7 @@
  36.110          val {params = (ps, qs), elems, ...} = the_locale thy name;
  36.111          val ps' = map (apsnd SOME o #1) ps;
  36.112          val ren = map #1 ps' ~~
  36.113 -              map (fn x => (x, valOf (Symtab.curried_lookup syn x))) xs;
  36.114 +              map (fn x => (x, valOf (Symtab.lookup syn x))) xs;
  36.115          val (params', elems') =
  36.116            if null ren then ((ps', qs), map #1 elems)
  36.117            else ((map (apfst (rename ren)) ps', map (rename ren) qs),
  36.118 @@ -1754,7 +1754,7 @@
  36.119          |> Symtab.make;            
  36.120      (* replace parameter names in ids by instantiations *)
  36.121      val vinst = Symtab.make (parms ~~ vts);
  36.122 -    fun vinst_names ps = map (the o Symtab.curried_lookup vinst) ps;
  36.123 +    fun vinst_names ps = map (the o Symtab.lookup vinst) ps;
  36.124      val inst = Symtab.make (parms ~~ ts);
  36.125      val ids' = map (apsnd vinst_names) ids;
  36.126      val wits = List.concat (map (snd o valOf o get_global_registration thy) ids');
  36.127 @@ -2028,7 +2028,7 @@
  36.128      |> put_locale name {predicate = predicate, import = import,
  36.129          elems = map (fn e => (e, stamp ())) elems',
  36.130          params = (params_of elemss' |>
  36.131 -          map (fn (x, SOME T) => ((x, T), the (Symtab.curried_lookup syn x))), map #1 (params_of body_elemss)),
  36.132 +          map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), map #1 (params_of body_elemss)),
  36.133          regs = []}
  36.134      |> pair (elems', body_ctxt)
  36.135    end;
  36.136 @@ -2264,7 +2264,7 @@
  36.137                 NONE => error ("Instance missing for parameter " ^ quote p)
  36.138               | SOME (Free (_, T), t) => (t, T);
  36.139          val d = inst_tab_term (inst, tinst) t;
  36.140 -      in (Symtab.curried_update_new (p, d) inst, tinst) end;
  36.141 +      in (Symtab.update_new (p, d) inst, tinst) end;
  36.142      val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given);
  36.143      (* Note: inst and tinst contain no vars. *)
  36.144  
    37.1 --- a/src/Pure/Isar/method.ML	Thu Sep 15 17:16:55 2005 +0200
    37.2 +++ b/src/Pure/Isar/method.ML	Thu Sep 15 17:16:56 2005 +0200
    37.3 @@ -570,7 +570,7 @@
    37.4          val ((raw_name, _), pos) = Args.dest_src src;
    37.5          val name = NameSpace.intern space raw_name;
    37.6        in
    37.7 -        (case Symtab.curried_lookup meths name of
    37.8 +        (case Symtab.lookup meths name of
    37.9            NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
   37.10          | SOME ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src))
   37.11        end;
    38.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Sep 15 17:16:55 2005 +0200
    38.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Sep 15 17:16:56 2005 +0200
    38.3 @@ -125,10 +125,10 @@
    38.4  
    38.5  fun get_lexicons () = ! global_lexicons;
    38.6  fun get_parsers () = ! global_parsers;
    38.7 -fun get_parser () = Option.map (#2 o #1) o Symtab.curried_lookup (get_parsers ());
    38.8 +fun get_parser () = Option.map (#2 o #1) o Symtab.lookup (get_parsers ());
    38.9  
   38.10  fun command_tags name =
   38.11 -  (case Symtab.curried_lookup (get_parsers ()) name of
   38.12 +  (case Symtab.lookup (get_parsers ()) name of
   38.13      SOME (((_, k), _), _) => OuterKeyword.tags_of k
   38.14    | NONE => []);
   38.15  
   38.16 @@ -143,7 +143,7 @@
   38.17  fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab =
   38.18   (if not (Symtab.defined tab name) then ()
   38.19    else warning ("Redefined outer syntax command " ^ quote name);
   38.20 -  Symtab.curried_update (name, (((comment, kind), (int_only, parse)), markup)) tab);
   38.21 +  Symtab.update (name, (((comment, kind), (int_only, parse)), markup)) tab);
   38.22  
   38.23  fun add_parsers parsers =
   38.24    (change_parsers (fold add_parser parsers);
    39.1 --- a/src/Pure/Isar/proof_context.ML	Thu Sep 15 17:16:55 2005 +0200
    39.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Sep 15 17:16:56 2005 +0200
    39.3 @@ -365,18 +365,18 @@
    39.4  
    39.5  (** default sorts and types **)
    39.6  
    39.7 -val def_sort = Vartab.curried_lookup o #2 o defaults_of;
    39.8 +val def_sort = Vartab.lookup o #2 o defaults_of;
    39.9  
   39.10  fun def_type ctxt pattern xi =
   39.11    let val {binds, defs = (types, _, _, _), ...} = rep_context ctxt in
   39.12 -    (case Vartab.curried_lookup types xi of
   39.13 +    (case Vartab.lookup types xi of
   39.14        NONE =>
   39.15          if pattern then NONE
   39.16 -        else Vartab.curried_lookup binds xi |> Option.map (TypeInfer.polymorphicT o #2)
   39.17 +        else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #2)
   39.18      | some => some)
   39.19    end;
   39.20  
   39.21 -fun default_type ctxt x = Vartab.curried_lookup (#1 (defaults_of ctxt)) (x, ~1);
   39.22 +fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt)) (x, ~1);
   39.23  val used_types = #3 o defaults_of;
   39.24  
   39.25  
   39.26 @@ -493,7 +493,7 @@
   39.27  
   39.28      val binds = binds_of ctxt;
   39.29      fun norm (t as Var (xi, T)) =
   39.30 -          (case Vartab.curried_lookup binds xi of
   39.31 +          (case Vartab.lookup binds xi of
   39.32              SOME (u, U) =>
   39.33                let
   39.34                  val env = unifyT ctxt (T, U) handle Type.TUNIFY =>
   39.35 @@ -597,24 +597,24 @@
   39.36  local
   39.37  
   39.38  val ins_types = fold_aterms
   39.39 -  (fn Free (x, T) => Vartab.curried_update ((x, ~1), T)
   39.40 -    | Var v => Vartab.curried_update v
   39.41 +  (fn Free (x, T) => Vartab.update ((x, ~1), T)
   39.42 +    | Var v => Vartab.update v
   39.43      | _ => I);
   39.44  
   39.45  val ins_sorts = fold_types (fold_atyps
   39.46 -  (fn TFree (x, S) => Vartab.curried_update ((x, ~1), S)
   39.47 -    | TVar v => Vartab.curried_update v
   39.48 +  (fn TFree (x, S) => Vartab.update ((x, ~1), S)
   39.49 +    | TVar v => Vartab.update v
   39.50      | _ => I));
   39.51  
   39.52  val ins_used = fold_term_types (fn t =>
   39.53    fold_atyps (fn TFree (x, _) => insert (op =) x | _ => I));
   39.54  
   39.55  val ins_occs = fold_term_types (fn t =>
   39.56 -  fold_atyps (fn TFree (x, _) => Symtab.curried_update_multi (x, t) | _ => I));
   39.57 +  fold_atyps (fn TFree (x, _) => Symtab.update_multi (x, t) | _ => I));
   39.58  
   39.59  fun ins_skolem def_ty = fold_rev (fn (x, x') =>
   39.60    (case def_ty x' of
   39.61 -    SOME T => Vartab.curried_update ((x, ~1), T)
   39.62 +    SOME T => Vartab.update ((x, ~1), T)
   39.63    | NONE => I));
   39.64  
   39.65  fun map_defaults f = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
   39.66 @@ -633,7 +633,7 @@
   39.67    |> declare_term_syntax t
   39.68    |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs t occ))
   39.69    |> map_defaults (fn (types, sorts, used, occ) =>
   39.70 -      (ins_skolem (fn x => Vartab.curried_lookup types (x, ~1)) (fixes_of ctxt) types,
   39.71 +      (ins_skolem (fn x => Vartab.lookup types (x, ~1)) (fixes_of ctxt) types,
   39.72          sorts, used, occ));
   39.73  
   39.74  end;
   39.75 @@ -691,7 +691,7 @@
   39.76      val occs_outer = type_occs_of outer;
   39.77      fun add a gen =
   39.78        if Symtab.defined occs_outer a orelse
   39.79 -        exists still_fixed (Symtab.curried_lookup_multi occs_inner a)
   39.80 +        exists still_fixed (Symtab.lookup_multi occs_inner a)
   39.81        then gen else a :: gen;
   39.82    in fn tfrees => fold add tfrees [] end;
   39.83  
   39.84 @@ -774,7 +774,7 @@
   39.85        else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
   39.86    in
   39.87      map_context (fn (syntax, asms, binds, thms, cases, defs) =>
   39.88 -      (syntax, asms, Vartab.curried_update ((x, i), (t', T)) binds, thms, cases, defs))
   39.89 +      (syntax, asms, Vartab.update ((x, i), (t', T)) binds, thms, cases, defs))
   39.90      o declare_term t'
   39.91    end;
   39.92  
   39.93 @@ -932,7 +932,7 @@
   39.94          val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref;
   39.95          val name = PureThy.name_of_thmref thmref;
   39.96        in
   39.97 -        (case Symtab.curried_lookup tab name of
   39.98 +        (case Symtab.lookup tab name of
   39.99            SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths)
  39.100          | NONE => from_thy thy xthmref) |> pick name
  39.101        end
  39.102 @@ -993,7 +993,7 @@
  39.103          let
  39.104            val name = NameSpace.full naming bname;
  39.105            val space' = NameSpace.declare naming name space;
  39.106 -          val tab' = Symtab.curried_update (name, ths) tab;
  39.107 +          val tab' = Symtab.update (name, ths) tab;
  39.108            val index' = FactIndex.add (is_known ctxt) (name, ths) index;
  39.109          in (syntax, asms, binds, (naming, (space', tab'), index'), cases, defs) end);
  39.110  
    40.1 --- a/src/Pure/Isar/term_style.ML	Thu Sep 15 17:16:55 2005 +0200
    40.2 +++ b/src/Pure/Isar/term_style.ML	Thu Sep 15 17:16:56 2005 +0200
    40.3 @@ -40,12 +40,12 @@
    40.4  (* accessors *)
    40.5  
    40.6  fun the_style thy name =
    40.7 -  (case Symtab.curried_lookup (StyleData.get thy) name of
    40.8 +  (case Symtab.lookup (StyleData.get thy) name of
    40.9      NONE => error ("Unknown antiquote style: " ^ quote name)
   40.10    | SOME (style, _) => style);
   40.11  
   40.12  fun add_style name style thy =
   40.13 -  StyleData.map (Symtab.curried_update_new (name, (style, stamp ()))) thy
   40.14 +  StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
   40.15      handle Symtab.DUP _ => err_dup_styles [name];
   40.16  
   40.17  
    41.1 --- a/src/Pure/Proof/extraction.ML	Thu Sep 15 17:16:55 2005 +0200
    41.2 +++ b/src/Pure/Proof/extraction.ML	Thu Sep 15 17:16:56 2005 +0200
    41.3 @@ -301,7 +301,7 @@
    41.4    in
    41.5      ExtractionData.put
    41.6        {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
    41.7 -       realizers = fold (Symtab.curried_update_multi o prep_rlz thy) rs realizers,
    41.8 +       realizers = fold (Symtab.update_multi o prep_rlz thy) rs realizers,
    41.9         defs = defs, expand = expand, prep = prep} thy
   41.10    end
   41.11  
   41.12 @@ -564,7 +564,7 @@
   41.13                else fst (extr d defs vs ts Ts hs prf0)
   41.14            in
   41.15              if T = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0)
   41.16 -            else case Symtab.curried_lookup realizers name of
   41.17 +            else case Symtab.lookup realizers name of
   41.18                NONE => (case find vs' (find' name defs') of
   41.19                  NONE =>
   41.20                    let
   41.21 @@ -600,7 +600,7 @@
   41.22            in
   41.23              if etype_of thy' vs' [] prop = nullT andalso
   41.24                realizes_null vs' prop aconv prop then (defs, prf0)
   41.25 -            else case find vs' (Symtab.curried_lookup_multi realizers s) of
   41.26 +            else case find vs' (Symtab.lookup_multi realizers s) of
   41.27                SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
   41.28              | NONE => error ("corr: no realizer for instance of axiom " ^
   41.29                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   41.30 @@ -648,7 +648,7 @@
   41.31              val (vs', tye) = find_inst prop Ts ts vs;
   41.32              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
   41.33            in
   41.34 -            case Symtab.curried_lookup realizers s of
   41.35 +            case Symtab.lookup realizers s of
   41.36                NONE => (case find vs' (find' s defs) of
   41.37                  NONE =>
   41.38                    let
   41.39 @@ -707,7 +707,7 @@
   41.40              val (vs', tye) = find_inst prop Ts ts vs;
   41.41              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
   41.42            in
   41.43 -            case find vs' (Symtab.curried_lookup_multi realizers s) of
   41.44 +            case find vs' (Symtab.lookup_multi realizers s) of
   41.45                SOME (t, _) => (defs, subst_TVars tye' t)
   41.46              | NONE => error ("extr: no realizer for instance of axiom " ^
   41.47                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
    42.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu Sep 15 17:16:55 2005 +0200
    42.2 +++ b/src/Pure/Proof/proof_syntax.ML	Thu Sep 15 17:16:56 2005 +0200
    42.3 @@ -100,7 +100,7 @@
    42.4        let val prop = if_none (AList.lookup (op =) thms' key) (Bound 0)
    42.5        in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
    42.6          if prop <> prop' then
    42.7 -          (Symtab.curried_update (key ^ "_" ^ string_of_int i, prf) tab, i+1)
    42.8 +          (Symtab.update (key ^ "_" ^ string_of_int i, prf) tab, i+1)
    42.9          else x) (tab, 1) ps)
   42.10        end) (Symtab.empty, thms);
   42.11  
   42.12 @@ -111,7 +111,7 @@
   42.13        | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
   42.14            let
   42.15              val prop' = if_none (AList.lookup (op =) thms' s) (Bound 0);
   42.16 -            val ps = map fst (the (Symtab.curried_lookup thms s)) \ prop'
   42.17 +            val ps = map fst (the (Symtab.lookup thms s)) \ prop'
   42.18            in if prop = prop' then prf' else
   42.19              PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
   42.20                prf, prop, Ts)
   42.21 @@ -146,7 +146,7 @@
   42.22                   let val name = NameSpace.pack xs;
   42.23                   in (case AList.lookup (op =) thms name of
   42.24                       SOME thm => fst (strip_combt (Thm.proof_of thm))
   42.25 -                   | NONE => (case Symtab.curried_lookup tab name of
   42.26 +                   | NONE => (case Symtab.lookup tab name of
   42.27                           SOME prf => prf
   42.28                         | NONE => error ("Unknown theorem " ^ quote name)))
   42.29                   end
    43.1 --- a/src/Pure/Proof/proofchecker.ML	Thu Sep 15 17:16:55 2005 +0200
    43.2 +++ b/src/Pure/Proof/proofchecker.ML	Thu Sep 15 17:16:56 2005 +0200
    43.3 @@ -19,9 +19,9 @@
    43.4  (***** construct a theorem out of a proof term *****)
    43.5  
    43.6  fun lookup_thm thy =
    43.7 -  let val tab = fold_rev Symtab.curried_update (PureThy.all_thms_of thy) Symtab.empty
    43.8 +  let val tab = fold_rev Symtab.update (PureThy.all_thms_of thy) Symtab.empty
    43.9    in
   43.10 -    (fn s => case Symtab.curried_lookup tab s of
   43.11 +    (fn s => case Symtab.lookup tab s of
   43.12         NONE => error ("Unknown theorem " ^ quote s)
   43.13       | SOME thm => thm)
   43.14    end;
    44.1 --- a/src/Pure/Proof/reconstruct.ML	Thu Sep 15 17:16:55 2005 +0200
    44.2 +++ b/src/Pure/Proof/reconstruct.ML	Thu Sep 15 17:16:56 2005 +0200
    44.3 @@ -81,10 +81,10 @@
    44.4              end)
    44.5        else (t, T, vTs, env)
    44.6    | infer_type sg env Ts vTs (t as Free (s, T)) =
    44.7 -      if T = dummyT then (case Symtab.curried_lookup vTs s of
    44.8 +      if T = dummyT then (case Symtab.lookup vTs s of
    44.9            NONE =>
   44.10              let val (env', T) = mk_tvar (env, [])
   44.11 -            in (Free (s, T), T, Symtab.curried_update_new (s, T) vTs, env') end
   44.12 +            in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end
   44.13          | SOME T => (Free (s, T), T, vTs, env))
   44.14        else (t, T, vTs, env)
   44.15    | infer_type sg env Ts vTs (Var _) = error "reconstruct_proof: internal error"
    45.1 --- a/src/Pure/Syntax/ast.ML	Thu Sep 15 17:16:55 2005 +0200
    45.2 +++ b/src/Pure/Syntax/ast.ML	Thu Sep 15 17:16:56 2005 +0200
    45.3 @@ -157,7 +157,7 @@
    45.4            if a = b then env else raise NO_MATCH
    45.5        | mtch (Variable a) (Constant b) env =
    45.6            if a = b then env else raise NO_MATCH
    45.7 -      | mtch ast (Variable x) env = Symtab.curried_update (x, ast) env
    45.8 +      | mtch ast (Variable x) env = Symtab.update (x, ast) env
    45.9        | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env
   45.10        | mtch _ _ _ = raise NO_MATCH
   45.11      and mtch_lst (ast :: asts) (pat :: pats) env =
   45.12 @@ -189,7 +189,7 @@
   45.13      val changes = ref 0;
   45.14  
   45.15      fun subst _ (ast as Constant _) = ast
   45.16 -      | subst env (Variable x) = the (Symtab.curried_lookup env x)
   45.17 +      | subst env (Variable x) = the (Symtab.lookup env x)
   45.18        | subst env (Appl asts) = Appl (map (subst env) asts);
   45.19  
   45.20      fun try_rules ((lhs, rhs) :: pats) ast =
    46.1 --- a/src/Pure/Syntax/parser.ML	Thu Sep 15 17:16:55 2005 +0200
    46.2 +++ b/src/Pure/Syntax/parser.ML	Thu Sep 15 17:16:56 2005 +0200
    46.3 @@ -446,9 +446,9 @@
    46.4    let
    46.5      (*Get tag for existing nonterminal or create a new one*)
    46.6      fun get_tag nt_count tags nt =
    46.7 -      case Symtab.curried_lookup tags nt of
    46.8 +      case Symtab.lookup tags nt of
    46.9          SOME tag => (nt_count, tags, tag)
   46.10 -      | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags,
   46.11 +      | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
   46.12                   nt_count);
   46.13  
   46.14      (*Convert symbols to the form used by the parser;
   46.15 @@ -523,9 +523,9 @@
   46.16  
   46.17      (*get existing tag from grammar1 or create a new one*)
   46.18      fun get_tag nt_count tags nt =
   46.19 -      case Symtab.curried_lookup tags nt of
   46.20 +      case Symtab.lookup tags nt of
   46.21          SOME tag => (nt_count, tags, tag)
   46.22 -      | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags,
   46.23 +      | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
   46.24                  nt_count)
   46.25  
   46.26      val ((nt_count1', tags1'), tag_table) =
   46.27 @@ -868,7 +868,7 @@
   46.28  
   46.29  fun earley prods tags chains startsymbol indata =
   46.30    let
   46.31 -    val start_tag = case Symtab.curried_lookup tags startsymbol of
   46.32 +    val start_tag = case Symtab.lookup tags startsymbol of
   46.33                         SOME tag => tag
   46.34                       | NONE   => error ("parse: Unknown startsymbol " ^
   46.35                                          quote startsymbol);
    47.1 --- a/src/Pure/Syntax/printer.ML	Thu Sep 15 17:16:55 2005 +0200
    47.2 +++ b/src/Pure/Syntax/printer.ML	Thu Sep 15 17:16:56 2005 +0200
    47.3 @@ -248,7 +248,7 @@
    47.4      val tab = fold f fmts (mode_tab prtabs mode);
    47.5    in AList.update (op =) (mode, tab) prtabs end;
    47.6  
    47.7 -fun extend_prtabs m = change_prtabs Symtab.curried_update_multi m;
    47.8 +fun extend_prtabs m = change_prtabs Symtab.update_multi m;
    47.9  fun remove_prtabs m = change_prtabs (Symtab.remove_multi (op =)) m;
   47.10  
   47.11  fun merge_prtabs prtabs1 prtabs2 =
   47.12 @@ -330,7 +330,7 @@
   47.13  
   47.14          (*find matching table entry, or print as prefix / postfix*)
   47.15          fun prnt ([], []) = prefixT tup
   47.16 -          | prnt ([], tb :: tbs) = prnt (Symtab.curried_lookup_multi tb a, tbs)
   47.17 +          | prnt ([], tb :: tbs) = prnt (Symtab.lookup_multi tb a, tbs)
   47.18            | prnt ((pr, n, p') :: prnps, tbs) =
   47.19                if nargs = n then parT (pr, args, p, p')
   47.20                else if nargs > n andalso not type_mode then
    48.1 --- a/src/Pure/Syntax/syntax.ML	Thu Sep 15 17:16:55 2005 +0200
    48.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Sep 15 17:16:56 2005 +0200
    48.3 @@ -82,7 +82,7 @@
    48.4  
    48.5  (* parse (ast) translations *)
    48.6  
    48.7 -fun lookup_tr tab c = Option.map fst (Symtab.curried_lookup tab c);
    48.8 +fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
    48.9  
   48.10  fun err_dup_trfuns name cs =
   48.11    error ("More than one " ^ name ^ " for " ^ commas_quote cs);
   48.12 @@ -98,8 +98,8 @@
   48.13  
   48.14  (* print (ast) translations *)
   48.15  
   48.16 -fun lookup_tr' tab c = map fst (Symtab.curried_lookup_multi tab c);
   48.17 -fun extend_tr'tab trfuns = fold_rev Symtab.curried_update_multi trfuns;
   48.18 +fun lookup_tr' tab c = map fst (Symtab.lookup_multi tab c);
   48.19 +fun extend_tr'tab trfuns = fold_rev Symtab.update_multi trfuns;
   48.20  fun remove_tr'tab trfuns = fold (Symtab.remove_multi SynExt.eq_trfun) trfuns;
   48.21  fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' SynExt.eq_trfun (tab1, tab2);
   48.22  
   48.23 @@ -151,7 +151,7 @@
   48.24  
   48.25  (* empty, extend, merge ruletabs *)
   48.26  
   48.27 -val extend_ruletab = fold_rev (fn r => Symtab.curried_update_multi (Ast.head_of_rule r, r));
   48.28 +val extend_ruletab = fold_rev (fn r => Symtab.update_multi (Ast.head_of_rule r, r));
   48.29  val remove_ruletab = fold (fn r => Symtab.remove_multi (op =) (Ast.head_of_rule r, r));
   48.30  fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
   48.31  
   48.32 @@ -385,7 +385,7 @@
   48.33      val asts = read_asts thy is_logtype syn false (SynExt.typ_to_nonterm ty) str;
   48.34    in
   48.35      SynTrans.asts_to_terms thy (lookup_tr parse_trtab)
   48.36 -      (map (Ast.normalize_ast (Symtab.curried_lookup_multi parse_ruletab)) asts)
   48.37 +      (map (Ast.normalize_ast (Symtab.lookup_multi parse_ruletab)) asts)
   48.38    end;
   48.39  
   48.40  
   48.41 @@ -469,7 +469,7 @@
   48.42    in
   48.43      prt_t thy curried prtabs (lookup_tr' print_ast_trtab)
   48.44        (lookup_tokentr tokentrtab (! print_mode))
   48.45 -      (Ast.normalize_ast (Symtab.curried_lookup_multi print_ruletab) ast)
   48.46 +      (Ast.normalize_ast (Symtab.lookup_multi print_ruletab) ast)
   48.47    end;
   48.48  
   48.49  val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast;
    49.1 --- a/src/Pure/Thy/html.ML	Thu Sep 15 17:16:55 2005 +0200
    49.2 +++ b/src/Pure/Thy/html.ML	Thu Sep 15 17:16:56 2005 +0200
    49.3 @@ -205,7 +205,7 @@
    49.4    fun output_sym s =
    49.5      if Symbol.is_raw s then (1.0, Symbol.decode_raw s)
    49.6      else
    49.7 -      (case Symtab.curried_lookup html_syms s of SOME x => x
    49.8 +      (case Symtab.lookup html_syms s of SOME x => x
    49.9        | NONE => (real (size s), translate_string escape s));
   49.10  
   49.11    fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
    50.1 --- a/src/Pure/Thy/present.ML	Thu Sep 15 17:16:55 2005 +0200
    50.2 +++ b/src/Pure/Thy/present.ML	Thu Sep 15 17:16:56 2005 +0200
    50.3 @@ -172,13 +172,13 @@
    50.4  
    50.5  fun init_theory_info name info =
    50.6    change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
    50.7 -    (Symtab.curried_update (name, info) theories, files, tex_index, html_index, graph));
    50.8 +    (Symtab.update (name, info) theories, files, tex_index, html_index, graph));
    50.9  
   50.10  fun change_theory_info name f =
   50.11    change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) =>
   50.12 -    (case Symtab.curried_lookup theories name of
   50.13 +    (case Symtab.lookup theories name of
   50.14        NONE => (warning ("Browser info: cannot access theory document " ^ quote name); info)
   50.15 -    | SOME info => (Symtab.curried_update (name, map_theory_info f info) theories, files,
   50.16 +    | SOME info => (Symtab.update (name, map_theory_info f info) theories, files,
   50.17          tex_index, html_index, graph)));
   50.18  
   50.19  
    51.1 --- a/src/Pure/Thy/thm_database.ML	Thu Sep 15 17:16:55 2005 +0200
    51.2 +++ b/src/Pure/Thy/thm_database.ML	Thu Sep 15 17:16:56 2005 +0200
    51.3 @@ -88,7 +88,7 @@
    51.4          fun result prfx bname =
    51.5            if (prfx = "" orelse is_ml_identifier prfx) andalso is_ml_identifier bname andalso
    51.6                NameSpace.intern space xname = name then
    51.7 -            SOME (prfx, (bname, xname, length (the (Symtab.curried_lookup thms name)) = 1))
    51.8 +            SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1))
    51.9            else NONE;
   51.10          val names = NameSpace.unpack name;
   51.11        in
    52.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Sep 15 17:16:55 2005 +0200
    52.2 +++ b/src/Pure/Thy/thm_deps.ML	Thu Sep 15 17:16:56 2005 +0200
    52.3 @@ -55,7 +55,7 @@
    52.4                   | _ => ["global"]);
    52.5              in
    52.6                if name mem parents' then (gra', parents union parents')
    52.7 -              else (Symtab.curried_update (name,
    52.8 +              else (Symtab.update (name,
    52.9                  {name = Sign.base_name name, ID = name,
   52.10                   dir = space_implode "/" (session @ prefx),
   52.11                   unfold = false, path = "", parents = parents'}) gra',
    53.1 --- a/src/Pure/Thy/thy_parse.ML	Thu Sep 15 17:16:55 2005 +0200
    53.2 +++ b/src/Pure/Thy/thy_parse.ML	Thu Sep 15 17:16:56 2005 +0200
    53.3 @@ -469,7 +469,7 @@
    53.4    end;
    53.5  
    53.6  fun sect tab ((Keyword, s, n) :: toks) =
    53.7 -      (case Symtab.curried_lookup tab s of
    53.8 +      (case Symtab.lookup tab s of
    53.9          SOME parse => !! parse toks
   53.10        | NONE => syn_err "section" s n)
   53.11    | sect _ ((_, s, n) :: _) = syn_err "section" s n
    54.1 --- a/src/Pure/Tools/am_interpreter.ML	Thu Sep 15 17:16:55 2005 +0200
    54.2 +++ b/src/Pure/Tools/am_interpreter.ML	Thu Sep 15 17:16:56 2005 +0200
    54.3 @@ -107,7 +107,7 @@
    54.4  fun match_closure prog clos =
    54.5      case len_head_of_closure 0 clos of
    54.6          (len, CConst c) =>
    54.7 -        (case prog_struct.lookup (prog, (c, len)) of
    54.8 +        (case prog_struct.lookup prog (c, len) of
    54.9              NONE => NONE
   54.10            | SOME rules => match_rules 0 rules clos)
   54.11        | _ => NONE
    55.1 --- a/src/Pure/Tools/compute.ML	Thu Sep 15 17:16:55 2005 +0200
    55.2 +++ b/src/Pure/Tools/compute.ML	Thu Sep 15 17:16:56 2005 +0200
    55.3 @@ -44,13 +44,13 @@
    55.4  val remove_types =
    55.5      let
    55.6          fun remove_types_var table invtable ccount vcount ldepth t =
    55.7 -            (case Termtab.curried_lookup table t of
    55.8 +            (case Termtab.lookup table t of
    55.9                   NONE =>
   55.10                   let
   55.11                       val a = AbstractMachine.Var vcount
   55.12                   in
   55.13 -                     (Termtab.curried_update (t, a) table,
   55.14 -                      AMTermTab.curried_update (a, t) invtable,
   55.15 +                     (Termtab.update (t, a) table,
   55.16 +                      AMTermTab.update (a, t) invtable,
   55.17                        ccount,
   55.18                        inc vcount,
   55.19                        AbstractMachine.Var (add vcount ldepth))
   55.20 @@ -60,13 +60,13 @@
   55.21                 | SOME _ => sys_error "remove_types_var: lookup should be a var")
   55.22  
   55.23          fun remove_types_const table invtable ccount vcount ldepth t =
   55.24 -            (case Termtab.curried_lookup table t of
   55.25 +            (case Termtab.lookup table t of
   55.26                   NONE =>
   55.27                   let
   55.28                       val a = AbstractMachine.Const ccount
   55.29                   in
   55.30 -                     (Termtab.curried_update (t, a) table,
   55.31 -                      AMTermTab.curried_update (a, t) invtable,
   55.32 +                     (Termtab.update (t, a) table,
   55.33 +                      AMTermTab.update (a, t) invtable,
   55.34                        inc ccount,
   55.35                        vcount,
   55.36                        a)
   55.37 @@ -114,12 +114,12 @@
   55.38      let
   55.39          fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) =
   55.40              if v < ldepth then (Bound v, List.nth (bounds, v)) else
   55.41 -            (case AMTermTab.curried_lookup invtable (AbstractMachine.Var (v-ldepth)) of
   55.42 +            (case AMTermTab.lookup invtable (AbstractMachine.Var (v-ldepth)) of
   55.43                   SOME (t as Var (_, ty)) => (t, ty)
   55.44                 | SOME (t as Free (_, ty)) => (t, ty)
   55.45                 | _ => sys_error "infer_types: lookup should deliver Var or Free")
   55.46            | infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) =
   55.47 -            (case AMTermTab.curried_lookup invtable c of
   55.48 +            (case AMTermTab.lookup invtable c of
   55.49                   SOME (c as Const (_, ty)) => (c, ty)
   55.50                 | _ => sys_error "infer_types: lookup should deliver Const")
   55.51            | infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) =
   55.52 @@ -176,10 +176,10 @@
   55.53  
   55.54                  fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =
   55.55                      let
   55.56 -                        val var' = valOf (AMTermTab.curried_lookup invtable var)
   55.57 +                        val var' = valOf (AMTermTab.lookup invtable var)
   55.58                          val table = Termtab.delete var' table
   55.59                          val invtable = AMTermTab.delete var invtable
   55.60 -                        val vars = Inttab.curried_update_new (v, n) vars handle Inttab.DUP _ =>
   55.61 +                        val vars = Inttab.update_new (v, n) vars handle Inttab.DUP _ =>
   55.62                            raise (Make "no duplicate variable in pattern allowed")
   55.63                      in
   55.64                          (table, invtable, n+1, vars, AbstractMachine.PVar)
   55.65 @@ -217,7 +217,7 @@
   55.66  
   55.67                  fun rename ldepth vars (var as AbstractMachine.Var v) =
   55.68                      if v < ldepth then var
   55.69 -                    else (case Inttab.curried_lookup vars (v - ldepth) of
   55.70 +                    else (case Inttab.lookup vars (v - ldepth) of
   55.71                                NONE => raise (Make "new variable on right hand side")
   55.72                              | SOME n => AbstractMachine.Var ((vcount-n-1)+ldepth))
   55.73                    | rename ldepth vars (c as AbstractMachine.Const _) = c
    56.1 --- a/src/Pure/axclass.ML	Thu Sep 15 17:16:55 2005 +0200
    56.2 +++ b/src/Pure/axclass.ML	Thu Sep 15 17:16:56 2005 +0200
    56.3 @@ -148,7 +148,7 @@
    56.4  
    56.5  (* get and put data *)
    56.6  
    56.7 -val lookup_info = Symtab.curried_lookup o AxclassesData.get;
    56.8 +val lookup_info = Symtab.lookup o AxclassesData.get;
    56.9  
   56.10  fun get_info thy c =
   56.11    (case lookup_info thy c of
   56.12 @@ -220,7 +220,7 @@
   56.13        axms_thy
   56.14        |> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts))
   56.15        |> Theory.restore_naming class_thy
   56.16 -      |> AxclassesData.map (Symtab.curried_update (class, info));
   56.17 +      |> AxclassesData.map (Symtab.update (class, info));
   56.18    in (final_thy, {intro = intro, axioms = axioms}) end;
   56.19  
   56.20  in
    57.1 --- a/src/Pure/codegen.ML	Thu Sep 15 17:16:55 2005 +0200
    57.2 +++ b/src/Pure/codegen.ML	Thu Sep 15 17:16:56 2005 +0200
    57.3 @@ -427,13 +427,13 @@
    57.4            let
    57.5              val s' = NameSpace.pack ys
    57.6              val s'' = NameSpace.append module s'
    57.7 -          in case Symtab.curried_lookup used s'' of
    57.8 +          in case Symtab.lookup used s'' of
    57.9                NONE => ((module, s'),
   57.10 -                (Symtab.curried_update_new (s, (module, s')) tab,
   57.11 -                 Symtab.curried_update_new (s'', ()) used))
   57.12 +                (Symtab.update_new (s, (module, s')) tab,
   57.13 +                 Symtab.update_new (s'', ()) used))
   57.14              | SOME _ => find_name yss
   57.15            end
   57.16 -  in case Symtab.curried_lookup tab s of
   57.17 +  in case Symtab.lookup tab s of
   57.18        NONE => find_name (Library.suffixes1 (NameSpace.unpack s))
   57.19      | SOME name => (name, p)
   57.20    end;
   57.21 @@ -453,7 +453,7 @@
   57.22    in ((gr, (tab1', tab2)), (module, s'')) end;
   57.23  
   57.24  fun get_const_id cname (gr, (tab1, tab2)) =
   57.25 -  case Symtab.curried_lookup (fst tab1) cname of
   57.26 +  case Symtab.lookup (fst tab1) cname of
   57.27      NONE => error ("get_const_id: no such constant: " ^ quote cname)
   57.28    | SOME (module, s) =>
   57.29        let
   57.30 @@ -469,7 +469,7 @@
   57.31    in ((gr, (tab1, tab2')), (module, s'')) end;
   57.32  
   57.33  fun get_type_id tyname (gr, (tab1, tab2)) =
   57.34 -  case Symtab.curried_lookup (fst tab2) tyname of
   57.35 +  case Symtab.lookup (fst tab2) tyname of
   57.36      NONE => error ("get_type_id: no such type: " ^ quote tyname)
   57.37    | SOME (module, s) =>
   57.38        let
   57.39 @@ -557,15 +557,15 @@
   57.40          NONE => defs
   57.41        | SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of
   57.42            NONE => defs
   57.43 -        | SOME (s, (T, (args, rhs))) => Symtab.curried_update
   57.44 +        | SOME (s, (T, (args, rhs))) => Symtab.update
   57.45              (s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) ::
   57.46 -            if_none (Symtab.curried_lookup defs s) []) defs))
   57.47 +            if_none (Symtab.lookup defs s) []) defs))
   57.48    in
   57.49      foldl (fn ((thyname, axms), defs) =>
   57.50        Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss
   57.51    end;
   57.52  
   57.53 -fun get_defn thy defs s T = (case Symtab.curried_lookup defs s of
   57.54 +fun get_defn thy defs s T = (case Symtab.lookup defs s of
   57.55      NONE => NONE
   57.56    | SOME ds =>
   57.57        let val i = find_index (is_instance thy T o fst) ds
   57.58 @@ -829,7 +829,7 @@
   57.59          (Graph.merge (fn ((_, module, _), (_, module', _)) =>
   57.60             module = module') (gr, gr'),
   57.61           (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr
   57.62 -           (map (fn s => case Symtab.curried_lookup graphs s of
   57.63 +           (map (fn s => case Symtab.lookup graphs s of
   57.64                  NONE => error ("Undefined code module: " ^ s)
   57.65                | SOME gr => gr) modules))
   57.66        handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks);
   57.67 @@ -1056,7 +1056,7 @@
   57.68                     "use \"" ^ name ^ ".ML\";\n") code)) :: code)
   57.69             else File.write (Path.unpack fname) (snd (hd code)));
   57.70             if lib then thy
   57.71 -           else map_modules (Symtab.curried_update (module, gr)) thy)
   57.72 +           else map_modules (Symtab.update (module, gr)) thy)
   57.73       end));
   57.74  
   57.75  val code_libraryP =
    58.1 --- a/src/Pure/compress.ML	Thu Sep 15 17:16:55 2005 +0200
    58.2 +++ b/src/Pure/compress.ML	Thu Sep 15 17:16:56 2005 +0200
    58.3 @@ -42,11 +42,11 @@
    58.4    let
    58.5      val typs = #1 (CompressData.get thy);
    58.6      fun compress T =
    58.7 -      (case Typtab.curried_lookup (! typs) T of
    58.8 +      (case Typtab.lookup (! typs) T of
    58.9          SOME T' => T'
   58.10        | NONE =>
   58.11            let val T' = (case T of Type (a, Ts) => Type (a, map compress Ts) | _ => T)
   58.12 -          in change typs (Typtab.curried_update (T', T')); T' end);
   58.13 +          in change typs (Typtab.update (T', T')); T' end);
   58.14    in compress end;
   58.15  
   58.16  
   58.17 @@ -58,9 +58,9 @@
   58.18      fun compress (t $ u) = compress t $ compress u
   58.19        | compress (Abs (a, T, t)) = Abs (a, T, compress t)
   58.20        | compress t =
   58.21 -          (case Termtab.curried_lookup (! terms) t of
   58.22 +          (case Termtab.lookup (! terms) t of
   58.23              SOME t' => t'
   58.24 -          | NONE => (change terms (Termtab.curried_update (t, t)); t));
   58.25 +          | NONE => (change terms (Termtab.update (t, t)); t));
   58.26    in compress o map_term_types (typ thy) end;
   58.27  
   58.28  end;
    59.1 --- a/src/Pure/context.ML	Thu Sep 15 17:16:55 2005 +0200
    59.2 +++ b/src/Pure/context.ML	Thu Sep 15 17:16:56 2005 +0200
    59.3 @@ -118,7 +118,7 @@
    59.4  val kinds = ref (Inttab.empty: kind Inttab.table);
    59.5  
    59.6  fun invoke meth_name meth_fn k =
    59.7 -  (case Inttab.curried_lookup (! kinds) k of
    59.8 +  (case Inttab.lookup (! kinds) k of
    59.9      SOME kind => meth_fn kind |> transform_failure (fn exn =>
   59.10        EXCEPTION (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   59.11    | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
   59.12 @@ -137,7 +137,7 @@
   59.13      val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge};
   59.14      val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
   59.15        warning ("Duplicate declaration of theory data " ^ quote name));
   59.16 -    val _ = change kinds (Inttab.curried_update (k, kind));
   59.17 +    val _ = change kinds (Inttab.update (k, kind));
   59.18    in k end;
   59.19  
   59.20  val copy_data = Inttab.map' invoke_copy;
   59.21 @@ -253,7 +253,7 @@
   59.22    if draft_id id orelse Inttab.defined ids (#1 id) then ids
   59.23    else if Inttab.exists (equal (#2 id) o #2) ids then
   59.24      raise TERM ("Different versions of theory component " ^ quote (#2 id), [])
   59.25 -  else Inttab.curried_update id ids;
   59.26 +  else Inttab.update id ids;
   59.27  
   59.28  fun check_insert intermediate id (ids, iids) =
   59.29    let val ids' = check_ins id ids and iids' = check_ins id iids
   59.30 @@ -420,12 +420,12 @@
   59.31  val declare = declare_theory_data;
   59.32  
   59.33  fun get k dest thy =
   59.34 -  (case Inttab.curried_lookup (#theory (data_of thy)) k of
   59.35 +  (case Inttab.lookup (#theory (data_of thy)) k of
   59.36      SOME x => (dest x handle Match =>
   59.37        error ("Failed to access theory data " ^ quote (invoke_name k)))
   59.38    | NONE => error ("Uninitialized theory data " ^ quote (invoke_name k)));
   59.39  
   59.40 -fun put k mk x = modify_thy (map_theory (Inttab.curried_update (k, mk x)));
   59.41 +fun put k mk x = modify_thy (map_theory (Inttab.update (k, mk x)));
   59.42  fun init k = put k I (invoke_empty k);
   59.43  
   59.44  end;
   59.45 @@ -522,7 +522,7 @@
   59.46  val kinds = ref (Inttab.empty: kind Inttab.table);
   59.47  
   59.48  fun invoke meth_name meth_fn k =
   59.49 -  (case Inttab.curried_lookup (! kinds) k of
   59.50 +  (case Inttab.lookup (! kinds) k of
   59.51      SOME kind => meth_fn kind |> transform_failure (fn exn =>
   59.52        EXCEPTION (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   59.53    | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
   59.54 @@ -546,18 +546,18 @@
   59.55      val kind = {name = name, init = init};
   59.56      val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
   59.57        warning ("Duplicate declaration of proof data " ^ quote name));
   59.58 -    val _ = change kinds (Inttab.curried_update (k, kind));
   59.59 +    val _ = change kinds (Inttab.update (k, kind));
   59.60    in k end;
   59.61  
   59.62 -fun init k = modify_thy (map_proof (Inttab.curried_update (k, ())));
   59.63 +fun init k = modify_thy (map_proof (Inttab.update (k, ())));
   59.64  
   59.65  fun get k dest prf =
   59.66 -  (case Inttab.curried_lookup (data_of_proof prf) k of
   59.67 +  (case Inttab.lookup (data_of_proof prf) k of
   59.68      SOME x => (dest x handle Match =>
   59.69        error ("Failed to access proof data " ^ quote (invoke_name k)))
   59.70    | NONE => error ("Uninitialized proof data " ^ quote (invoke_name k)));
   59.71  
   59.72 -fun put k mk x = map_prf (Inttab.curried_update (k, mk x));
   59.73 +fun put k mk x = map_prf (Inttab.update (k, mk x));
   59.74  
   59.75  end;
   59.76  
    60.1 --- a/src/Pure/defs.ML	Thu Sep 15 17:16:55 2005 +0200
    60.2 +++ b/src/Pure/defs.ML	Thu Sep 15 17:16:56 2005 +0200
    60.3 @@ -46,11 +46,11 @@
    60.4           typ  (* type of the constant in this particular definition *)
    60.5           * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *)
    60.6  
    60.7 -fun getnode graph = the o Symtab.curried_lookup graph
    60.8 +fun getnode graph = the o Symtab.lookup graph
    60.9  fun get_nodedefs (Node (_, defs, _, _, _)) = defs
   60.10 -fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.curried_lookup defs defname
   60.11 +fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup defs defname
   60.12  fun get_defnode' graph noderef =
   60.13 -  Symtab.curried_lookup (get_nodedefs (the (Symtab.curried_lookup graph noderef)))
   60.14 +  Symtab.lookup (get_nodedefs (the (Symtab.lookup graph noderef)))
   60.15  
   60.16  fun table_size table = Symtab.fold (K (fn x => x + 1)) table 0;
   60.17  
   60.18 @@ -94,7 +94,7 @@
   60.19          val tv = typ_tvars t
   60.20          val t' = Logic.incr_tvar inc t
   60.21          fun update_subst ((n, i), _) =
   60.22 -          Vartab.curried_update ((n, i), ([], TVar ((n, i + inc), [])));
   60.23 +          Vartab.update ((n, i), ([], TVar ((n, i + inc), [])));
   60.24        in
   60.25          (t', fold update_subst tv Vartab.empty)
   60.26        end
   60.27 @@ -157,9 +157,9 @@
   60.28              ((tab,max), []) ts
   60.29  
   60.30        fun idx (tab,max) (TVar ((a,i),_)) =
   60.31 -          (case Inttab.curried_lookup tab i of
   60.32 +          (case Inttab.lookup tab i of
   60.33               SOME j => ((tab, max), TVar ((a,j),[]))
   60.34 -           | NONE => ((Inttab.curried_update (i, max) tab, max + 1), TVar ((a,max),[])))
   60.35 +           | NONE => ((Inttab.update (i, max) tab, max + 1), TVar ((a,max),[])))
   60.36          | idx (tab,max) (Type (t, ts)) =
   60.37            let
   60.38              val ((tab, max), ts) = idxlist idx I fst (tab, max) ts
   60.39 @@ -207,10 +207,10 @@
   60.40  
   60.41  fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) =
   60.42      (cost, axmap, (Declare cty)::actions,
   60.43 -     Symtab.curried_update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph)
   60.44 +     Symtab.update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph)
   60.45      handle Symtab.DUP _ =>
   60.46             let
   60.47 -             val (Node (gty, _, _, _, _)) = the (Symtab.curried_lookup graph name)
   60.48 +             val (Node (gty, _, _, _, _)) = the (Symtab.lookup graph name)
   60.49             in
   60.50               if is_instance_r ty gty andalso is_instance_r gty ty then
   60.51                 g
   60.52 @@ -227,13 +227,13 @@
   60.53        val _ = axcounter := c+1
   60.54        val axname' = axname^"_"^(IntInf.toString c)
   60.55      in
   60.56 -      (Symtab.curried_update (axname', axname) axmap, axname')
   60.57 +      (Symtab.update (axname', axname) axmap, axname')
   60.58      end
   60.59  
   60.60  fun translate_ex axmap x =
   60.61      let
   60.62        fun translate (ty, nodename, axname) =
   60.63 -          (ty, nodename, the (Symtab.curried_lookup axmap axname))
   60.64 +          (ty, nodename, the (Symtab.lookup axmap axname))
   60.65      in
   60.66        case x of
   60.67          INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain))
   60.68 @@ -243,7 +243,7 @@
   60.69  
   60.70  fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body =
   60.71      let
   60.72 -      val mainnode  = (case Symtab.curried_lookup graph mainref of
   60.73 +      val mainnode  = (case Symtab.lookup graph mainref of
   60.74                           NONE => def_err ("constant "^mainref^" is not declared")
   60.75                         | SOME n => n)
   60.76        val (Node (gty, defs, backs, finals, _)) = mainnode
   60.77 @@ -273,8 +273,8 @@
   60.78               let
   60.79                 val links = map normalize_edge_idx links
   60.80               in
   60.81 -               Symtab.curried_update (nodename,
   60.82 -                               case Symtab.curried_lookup edges nodename of
   60.83 +               Symtab.update (nodename,
   60.84 +                               case Symtab.lookup edges nodename of
   60.85                                   NONE => links
   60.86                                 | SOME links' => merge_edges links' links) edges
   60.87               end)
   60.88 @@ -282,7 +282,7 @@
   60.89        fun make_edges ((bodyn, bodyty), edges) =
   60.90            let
   60.91              val bnode =
   60.92 -                (case Symtab.curried_lookup graph bodyn of
   60.93 +                (case Symtab.lookup graph bodyn of
   60.94                     NONE => def_err "body of constant definition references undeclared constant"
   60.95                   | SOME x => x)
   60.96              val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode
   60.97 @@ -345,13 +345,13 @@
   60.98                          sys_error ("install_backrefs: closed node cannot be updated")
   60.99                        else ()
  60.100                val defnames =
  60.101 -                  (case Symtab.curried_lookup backs mainref of
  60.102 +                  (case Symtab.lookup backs mainref of
  60.103                       NONE => Symtab.empty
  60.104                     | SOME s => s)
  60.105 -              val defnames' = Symtab.curried_update_new (axname, ()) defnames
  60.106 -              val backs' = Symtab.curried_update (mainref, defnames') backs
  60.107 +              val defnames' = Symtab.update_new (axname, ()) defnames
  60.108 +              val backs' = Symtab.update (mainref, defnames') backs
  60.109              in
  60.110 -              Symtab.curried_update (noderef, Node (ty, defs, backs', finals, closed)) graph
  60.111 +              Symtab.update (noderef, Node (ty, defs, backs', finals, closed)) graph
  60.112              end
  60.113            else
  60.114              graph
  60.115 @@ -364,7 +364,7 @@
  60.116            else if closed = Open andalso is_instance_r gty ty then Closed else closed
  60.117  
  60.118        val thisDefnode = Defnode (ty, edges)
  60.119 -      val graph = Symtab.curried_update (mainref, Node (gty, Symtab.curried_update_new
  60.120 +      val graph = Symtab.update (mainref, Node (gty, Symtab.update_new
  60.121          (axname, thisDefnode) defs, backs, finals, closed)) graph
  60.122  
  60.123        (* Now we have to check all backreferences to this node and inform them about
  60.124 @@ -377,8 +377,8 @@
  60.125                        getnode graph noderef
  60.126                    val _ = if closed = Final then sys_error "update_defs: closed node" else ()
  60.127                    val (Defnode (def_ty, defnode_edges)) =
  60.128 -                      the (Symtab.curried_lookup nodedefs defname)
  60.129 -                  val edges = the (Symtab.curried_lookup defnode_edges mainref)
  60.130 +                      the (Symtab.lookup nodedefs defname)
  60.131 +                  val edges = the (Symtab.lookup defnode_edges mainref)
  60.132                    val refclosed = ref false
  60.133  
  60.134                    (* the type of thisDefnode is ty *)
  60.135 @@ -416,7 +416,7 @@
  60.136                    val defnames' = if edges' = [] then
  60.137                                      defnames
  60.138                                    else
  60.139 -                                    Symtab.curried_update (defname, ()) defnames
  60.140 +                                    Symtab.update (defname, ()) defnames
  60.141                  in
  60.142                    if changed then
  60.143                      let
  60.144 @@ -424,14 +424,14 @@
  60.145                            if edges' = [] then
  60.146                              Symtab.delete mainref defnode_edges
  60.147                            else
  60.148 -                            Symtab.curried_update (mainref, edges') defnode_edges
  60.149 +                            Symtab.update (mainref, edges') defnode_edges
  60.150                        val defnode' = Defnode (def_ty, defnode_edges')
  60.151 -                      val nodedefs' = Symtab.curried_update (defname, defnode') nodedefs
  60.152 +                      val nodedefs' = Symtab.update (defname, defnode') nodedefs
  60.153                        val closed = if closed = Closed andalso Symtab.is_empty defnode_edges'
  60.154                                        andalso no_forwards nodedefs'
  60.155                                     then Final else closed
  60.156                        val graph' =
  60.157 -                        Symtab.curried_update
  60.158 +                        Symtab.update
  60.159                            (noderef, Node (nodety, nodedefs', nodebacks, nodefinals, closed)) graph
  60.160                      in
  60.161                        (defnames', graph')
  60.162 @@ -447,7 +447,7 @@
  60.163                (backs, graph')
  60.164              else
  60.165                let
  60.166 -                val backs' = Symtab.curried_update_new (noderef, defnames') backs
  60.167 +                val backs' = Symtab.update_new (noderef, defnames') backs
  60.168                in
  60.169                  (backs', graph')
  60.170                end
  60.171 @@ -458,7 +458,7 @@
  60.172        (* If a Circular exception is thrown then we never reach this point. *)
  60.173        val (Node (gty, defs, _, finals, closed)) = getnode graph mainref
  60.174        val closed = if closed = Closed andalso no_forwards defs then Final else closed
  60.175 -      val graph = Symtab.curried_update (mainref, Node (gty, defs, backs, finals, closed)) graph
  60.176 +      val graph = Symtab.update (mainref, Node (gty, defs, backs, finals, closed)) graph
  60.177        val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions
  60.178      in
  60.179        (cost+3, axmap, actions', graph)
  60.180 @@ -482,7 +482,7 @@
  60.181      end
  60.182  
  60.183  fun finalize' (cost, axmap, history, graph) (noderef, ty) =
  60.184 -    case Symtab.curried_lookup graph noderef of
  60.185 +    case Symtab.lookup graph noderef of
  60.186        NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
  60.187      | SOME (Node (nodety, defs, backs, finals, closed)) =>
  60.188        let
  60.189 @@ -519,7 +519,7 @@
  60.190              val closed = if closed = Open andalso is_instance_r nodety ty then
  60.191                             Closed else
  60.192                           closed
  60.193 -            val graph = Symtab.curried_update (noderef, Node (nodety, defs, backs, finals, closed)) graph
  60.194 +            val graph = Symtab.update (noderef, Node (nodety, defs, backs, finals, closed)) graph
  60.195  
  60.196              fun update_backref ((graph, backs), (backrefname, backdefnames)) =
  60.197                  let
  60.198 @@ -532,7 +532,7 @@
  60.199                              the (get_defnode backnode backdefname)
  60.200  
  60.201                          val (defnames', all_edges') =
  60.202 -                            case Symtab.curried_lookup all_edges noderef of
  60.203 +                            case Symtab.lookup all_edges noderef of
  60.204                                NONE => sys_error "finalize: corrupt backref"
  60.205                              | SOME edges =>
  60.206                                let
  60.207 @@ -542,11 +542,11 @@
  60.208                                  if edges' = [] then
  60.209                                    (defnames, Symtab.delete noderef all_edges)
  60.210                                  else
  60.211 -                                  (Symtab.curried_update (backdefname, ()) defnames,
  60.212 -                                   Symtab.curried_update (noderef, edges') all_edges)
  60.213 +                                  (Symtab.update (backdefname, ()) defnames,
  60.214 +                                   Symtab.update (noderef, edges') all_edges)
  60.215                                end
  60.216                          val defnode' = Defnode (def_ty, all_edges')
  60.217 -                        val backdefs' = Symtab.curried_update (backdefname, defnode') backdefs
  60.218 +                        val backdefs' = Symtab.update (backdefname, defnode') backdefs
  60.219                          val backclosed' = if backclosed = Closed andalso
  60.220                                               Symtab.is_empty all_edges'
  60.221                                               andalso no_forwards backdefs'
  60.222 @@ -554,19 +554,19 @@
  60.223                          val backnode' =
  60.224                              Node (backty, backdefs', backbacks, backfinals, backclosed')
  60.225                        in
  60.226 -                        (Symtab.curried_update (backrefname, backnode') graph, defnames')
  60.227 +                        (Symtab.update (backrefname, backnode') graph, defnames')
  60.228                        end
  60.229  
  60.230                    val (graph', defnames') =
  60.231                        Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
  60.232                  in
  60.233                    (graph', if Symtab.is_empty defnames' then backs
  60.234 -                           else Symtab.curried_update (backrefname, defnames') backs)
  60.235 +                           else Symtab.update (backrefname, defnames') backs)
  60.236                  end
  60.237              val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
  60.238              val Node ( _, defs, _, _, closed) = getnode graph' noderef
  60.239              val closed = if closed = Closed andalso no_forwards defs then Final else closed
  60.240 -            val graph' = Symtab.curried_update (noderef, Node (nodety, defs, backs',
  60.241 +            val graph' = Symtab.update (noderef, Node (nodety, defs, backs',
  60.242                                                          finals, closed)) graph'
  60.243              val history' = (Finalize (noderef, ty)) :: history
  60.244            in
  60.245 @@ -577,14 +577,14 @@
  60.246  fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty)
  60.247  
  60.248  fun update_axname ax orig_ax (cost, axmap, history, graph) =
  60.249 -  (cost, Symtab.curried_update (ax, orig_ax) axmap, history, graph)
  60.250 +  (cost, Symtab.update (ax, orig_ax) axmap, history, graph)
  60.251  
  60.252  fun merge' (Declare cty, g) = declare' g cty
  60.253    | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) =
  60.254 -    (case Symtab.curried_lookup graph name of
  60.255 +    (case Symtab.lookup graph name of
  60.256         NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
  60.257       | SOME (Node (_, defs, _, _, _)) =>
  60.258 -       (case Symtab.curried_lookup defs axname of
  60.259 +       (case Symtab.lookup defs axname of
  60.260            NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
  60.261          | SOME _ => g))
  60.262    | merge' (Finalize finals, g) = finalize' g finals
  60.263 @@ -598,14 +598,14 @@
  60.264  fun finals (_, _, history, graph) =
  60.265      Symtab.foldl
  60.266        (fn (finals, (name, Node(_, _, _, ftys, _))) =>
  60.267 -          Symtab.curried_update_new (name, ftys) finals)
  60.268 +          Symtab.update_new (name, ftys) finals)
  60.269        (Symtab.empty, graph)
  60.270  
  60.271  fun overloading_info (_, axmap, _, graph) c =
  60.272      let
  60.273 -      fun translate (ax, Defnode (ty, _)) = (the (Symtab.curried_lookup axmap ax), ty)
  60.274 +      fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup axmap ax), ty)
  60.275      in
  60.276 -      case Symtab.curried_lookup graph c of
  60.277 +      case Symtab.lookup graph c of
  60.278          NONE => NONE
  60.279        | SOME (Node (ty, defnodes, _, _, state)) =>
  60.280          SOME (ty, map translate (Symtab.dest defnodes), state)
  60.281 @@ -618,7 +618,7 @@
  60.282    | monomorphicT _ = false
  60.283  
  60.284  fun monomorphic (_, _, _, graph) c =
  60.285 -  (case Symtab.curried_lookup graph c of
  60.286 +  (case Symtab.lookup graph c of
  60.287      NONE => true
  60.288    | SOME (Node (ty, defnodes, _, _, _)) =>
  60.289        Symtab.min_key defnodes = Symtab.max_key defnodes andalso
    61.1 --- a/src/Pure/envir.ML	Thu Sep 15 17:16:55 2005 +0200
    61.2 +++ b/src/Pure/envir.ML	Thu Sep 15 17:16:56 2005 +0200
    61.3 @@ -73,7 +73,7 @@
    61.4    [T', T], []);
    61.5  
    61.6  fun gen_lookup f asol (xname, T) =
    61.7 -  (case Vartab.curried_lookup asol xname of
    61.8 +  (case Vartab.lookup asol xname of
    61.9       NONE => NONE
   61.10     | SOME (U, t) => if f (T, U) then SOME t
   61.11         else var_clash xname T U);
   61.12 @@ -92,7 +92,7 @@
   61.13  fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
   61.14  
   61.15  fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
   61.16 -  Envir{maxidx=maxidx, asol=Vartab.curried_update_new (xname, (T, t)) asol, iTs=iTs};
   61.17 +  Envir{maxidx=maxidx, asol=Vartab.update_new (xname, (T, t)) asol, iTs=iTs};
   61.18  
   61.19  (*The empty environment.  New variables will start with the given index+1.*)
   61.20  fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
    62.1 --- a/src/Pure/fact_index.ML	Thu Sep 15 17:16:55 2005 +0200
    62.2 +++ b/src/Pure/fact_index.ML	Thu Sep 15 17:16:56 2005 +0200
    62.3 @@ -55,7 +55,7 @@
    62.4  
    62.5  fun add pred (name, ths) (Index {next, facts, consts, frees}) =
    62.6    let
    62.7 -    fun upd a = Symtab.curried_update_multi (a, (next, (name, ths)));
    62.8 +    fun upd a = Symtab.update_multi (a, (next, (name, ths)));
    62.9      val (cs, xs) = fold (index_thm pred) ths ([], []);
   62.10    in
   62.11      Index {next = next + 1, facts = (name, ths) :: facts,
   62.12 @@ -74,7 +74,7 @@
   62.13  
   62.14  fun find idx ([], []) = facts idx
   62.15    | find (Index {consts, frees, ...}) (cs, xs) =
   62.16 -      (map (Symtab.curried_lookup_multi consts) cs @
   62.17 -        map (Symtab.curried_lookup_multi frees) xs) |> intersects |> map #2;
   62.18 +      (map (Symtab.lookup_multi consts) cs @
   62.19 +        map (Symtab.lookup_multi frees) xs) |> intersects |> map #2;
   62.20  
   62.21  end;
    63.1 --- a/src/Pure/goals.ML	Thu Sep 15 17:16:55 2005 +0200
    63.2 +++ b/src/Pure/goals.ML	Thu Sep 15 17:16:56 2005 +0200
    63.3 @@ -213,13 +213,13 @@
    63.4  
    63.5  (* access locales *)
    63.6  
    63.7 -val get_locale = Symtab.curried_lookup o #locales o LocalesData.get;
    63.8 +val get_locale = Symtab.lookup o #locales o LocalesData.get;
    63.9  
   63.10  fun put_locale (name, locale) thy =
   63.11    let
   63.12      val {space, locales, scope} = LocalesData.get thy;
   63.13      val space' = Sign.declare_name thy name space;
   63.14 -    val locales' = Symtab.curried_update (name, locale) locales;
   63.15 +    val locales' = Symtab.update (name, locale) locales;
   63.16    in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
   63.17  
   63.18  fun lookup_locale thy xname =
    64.1 --- a/src/Pure/net.ML	Thu Sep 15 17:16:55 2005 +0200
    64.2 +++ b/src/Pure/net.ML	Thu Sep 15 17:16:56 2005 +0200
    64.3 @@ -94,8 +94,8 @@
    64.4              Net{comb=comb, var=ins1(keys,var), atoms=atoms}
    64.5          | ins1 (AtomK a :: keys, Net{comb,var,atoms}) =
    64.6              let
    64.7 -              val net' = if_none (Symtab.curried_lookup atoms a) empty;
    64.8 -              val atoms' = Symtab.curried_update (a, ins1 (keys, net')) atoms;
    64.9 +              val net' = if_none (Symtab.lookup atoms a) empty;
   64.10 +              val atoms' = Symtab.update (a, ins1 (keys, net')) atoms;
   64.11              in  Net{comb=comb, var=var, atoms=atoms'}  end
   64.12    in  ins1 (keys,net)  end;
   64.13  
   64.14 @@ -126,12 +126,12 @@
   64.15              newnet{comb=comb, var=del1(keys,var), atoms=atoms}
   64.16          | del1 (AtomK a :: keys, Net{comb,var,atoms}) =
   64.17              let val atoms' =
   64.18 -              (case Symtab.curried_lookup atoms a of
   64.19 +              (case Symtab.lookup atoms a of
   64.20                  NONE => raise DELETE
   64.21                | SOME net' =>
   64.22                    (case del1 (keys, net') of
   64.23                      Leaf [] => Symtab.delete a atoms
   64.24 -                  | net'' => Symtab.curried_update (a, net'') atoms))
   64.25 +                  | net'' => Symtab.update (a, net'') atoms))
   64.26              in  newnet{comb=comb, var=var, atoms=atoms'}  end
   64.27    in  del1 (keys,net)  end;
   64.28  
   64.29 @@ -143,7 +143,7 @@
   64.30  exception ABSENT;
   64.31  
   64.32  fun the_atom atoms a =
   64.33 -  (case Symtab.curried_lookup atoms a of
   64.34 +  (case Symtab.lookup atoms a of
   64.35      NONE => raise ABSENT
   64.36    | SOME net => net);
   64.37  
   64.38 @@ -222,7 +222,7 @@
   64.39            subtr comb1 comb2
   64.40            #> subtr var1 var2
   64.41            #> Symtab.fold (fn (a, net) =>
   64.42 -            subtr (if_none (Symtab.curried_lookup atoms1 a) emptynet) net) atoms2
   64.43 +            subtr (if_none (Symtab.lookup atoms1 a) emptynet) net) atoms2
   64.44    in subtr net1 net2 [] end;
   64.45  
   64.46  fun entries net = subtract (K false) empty net;
    65.1 --- a/src/Pure/pattern.ML	Thu Sep 15 17:16:55 2005 +0200
    65.2 +++ b/src/Pure/pattern.ML	Thu Sep 15 17:16:56 2005 +0200
    65.3 @@ -357,7 +357,7 @@
    65.4            if loose_bvar(t,0) then raise MATCH
    65.5            else (case Envir.lookup' (insts, (ixn, T)) of
    65.6                    NONE => (typ_match thy (tyinsts, (T, fastype_of t)),
    65.7 -                           Vartab.curried_update_new (ixn, (T, t)) insts)
    65.8 +                           Vartab.update_new (ixn, (T, t)) insts)
    65.9                  | SOME u => if t aeconv u then instsp else raise MATCH)
   65.10        | (Free (a,T), Free (b,U)) =>
   65.11            if a=b then (typ_match thy (tyinsts,(T,U)), insts) else raise MATCH
   65.12 @@ -378,11 +378,11 @@
   65.13  fun match_bind(itms,binders,ixn,T,is,t) =
   65.14    let val js = loose_bnos t
   65.15    in if null is
   65.16 -     then if null js then Vartab.curried_update_new (ixn, (T, t)) itms else raise MATCH
   65.17 +     then if null js then Vartab.update_new (ixn, (T, t)) itms else raise MATCH
   65.18       else if js subset_int is
   65.19            then let val t' = if downto0(is,length binders - 1) then t
   65.20                              else mapbnd (idx is) t
   65.21 -               in Vartab.curried_update_new (ixn, (T, mkabs (binders, is, t'))) itms end
   65.22 +               in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end
   65.23            else raise MATCH
   65.24    end;
   65.25  
    66.1 --- a/src/Pure/proofterm.ML	Thu Sep 15 17:16:55 2005 +0200
    66.2 +++ b/src/Pure/proofterm.ML	Thu Sep 15 17:16:56 2005 +0200
    66.3 @@ -143,10 +143,10 @@
    66.4        | oras_of (prf % _) = oras_of prf
    66.5        | oras_of (prf1 %% prf2) = oras_of prf1 #> oras_of prf2
    66.6        | oras_of (PThm ((name, _), prf, prop, _)) = (fn tabs as (thms, oras) =>
    66.7 -          case Symtab.curried_lookup thms name of
    66.8 -            NONE => oras_of prf (Symtab.curried_update (name, [prop]) thms, oras)
    66.9 +          case Symtab.lookup thms name of
   66.10 +            NONE => oras_of prf (Symtab.update (name, [prop]) thms, oras)
   66.11            | SOME ps => if prop mem ps then tabs else
   66.12 -              oras_of prf (Symtab.curried_update (name, prop::ps) thms, oras))
   66.13 +              oras_of prf (Symtab.update (name, prop::ps) thms, oras))
   66.14        | oras_of (Oracle (s, prop, _)) =
   66.15            apsnd (OrdList.insert string_term_ord (s, prop))
   66.16        | oras_of (MinProof (thms, _, oras)) =
   66.17 @@ -162,10 +162,10 @@
   66.18    | thms_of_proof (prf1 %% prf2) = thms_of_proof prf1 #> thms_of_proof prf2
   66.19    | thms_of_proof (prf % _) = thms_of_proof prf
   66.20    | thms_of_proof (prf' as PThm ((s, _), prf, prop, _)) = (fn tab =>
   66.21 -      case Symtab.curried_lookup tab s of
   66.22 -        NONE => thms_of_proof prf (Symtab.curried_update (s, [(prop, prf')]) tab)
   66.23 +      case Symtab.lookup tab s of
   66.24 +        NONE => thms_of_proof prf (Symtab.update (s, [(prop, prf')]) tab)
   66.25        | SOME ps => if exists (equal prop o fst) ps then tab else
   66.26 -          thms_of_proof prf (Symtab.curried_update (s, (prop, prf')::ps) tab))
   66.27 +          thms_of_proof prf (Symtab.update (s, (prop, prf')::ps) tab))
   66.28    | thms_of_proof (MinProof (prfs, _, _)) = fold (thms_of_proof o proof_of_min_thm) prfs
   66.29    | thms_of_proof _ = I;
   66.30  
   66.31 @@ -173,7 +173,7 @@
   66.32    | axms_of_proof (AbsP (_, _, prf)) = axms_of_proof prf
   66.33    | axms_of_proof (prf1 %% prf2) = axms_of_proof prf1 #> axms_of_proof prf2
   66.34    | axms_of_proof (prf % _) = axms_of_proof prf
   66.35 -  | axms_of_proof (prf as PAxm (s, _, _)) = Symtab.curried_update (s, prf)
   66.36 +  | axms_of_proof (prf as PAxm (s, _, _)) = Symtab.update (s, prf)
   66.37    | axms_of_proof (MinProof (_, prfs, _)) = fold (axms_of_proof o proof_of_min_axm) prfs
   66.38    | axms_of_proof _ = I;
   66.39  
    67.1 --- a/src/Pure/sign.ML	Thu Sep 15 17:16:55 2005 +0200
    67.2 +++ b/src/Pure/sign.ML	Thu Sep 15 17:16:56 2005 +0200
    67.3 @@ -285,8 +285,8 @@
    67.4  
    67.5  fun const_constraint thy c =
    67.6    let val ((_, consts), constraints) = #consts (rep_sg thy) in
    67.7 -    (case Symtab.curried_lookup constraints c of
    67.8 -      NONE => Option.map #1 (Symtab.curried_lookup consts c)
    67.9 +    (case Symtab.lookup constraints c of
   67.10 +      NONE => Option.map #1 (Symtab.lookup consts c)
   67.11      | some => some)
   67.12    end;
   67.13  
   67.14 @@ -294,7 +294,7 @@
   67.15    (case const_constraint thy c of SOME T => T
   67.16    | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   67.17  
   67.18 -val const_type = Option.map #1 oo (Symtab.curried_lookup o #2 o #1 o #consts o rep_sg);
   67.19 +val const_type = Option.map #1 oo (Symtab.lookup o #2 o #1 o #consts o rep_sg);
   67.20  
   67.21  fun the_const_type thy c =
   67.22    (case const_type thy c of SOME T => T
   67.23 @@ -517,7 +517,7 @@
   67.24  
   67.25  fun read_tyname thy raw_c =
   67.26    let val c = intern_type thy raw_c in
   67.27 -    (case Symtab.curried_lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of
   67.28 +    (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of
   67.29        SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
   67.30      | _ => error ("Undeclared type constructor: " ^ quote c))
   67.31    end;
   67.32 @@ -717,7 +717,7 @@
   67.33        handle TYPE (msg, _, _) => error msg;
   67.34      val _ = cert_term thy (Const (c, T))
   67.35        handle TYPE (msg, _, _) => error msg;
   67.36 -  in thy |> map_consts (apsnd (Symtab.curried_update (c, T))) end;
   67.37 +  in thy |> map_consts (apsnd (Symtab.update (c, T))) end;
   67.38  
   67.39  val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort);
   67.40  val add_const_constraint_i = gen_add_constraint (K I) certify_typ;
    68.1 --- a/src/Pure/sorts.ML	Thu Sep 15 17:16:55 2005 +0200
    68.2 +++ b/src/Pure/sorts.ML	Thu Sep 15 17:16:56 2005 +0200
    68.3 @@ -180,7 +180,7 @@
    68.4  fun mg_domain (classes, arities) a S =
    68.5    let
    68.6      fun dom c =
    68.7 -      (case AList.lookup (op =) (Symtab.curried_lookup_multi arities a) c of
    68.8 +      (case AList.lookup (op =) (Symtab.lookup_multi arities a) c of
    68.9          NONE => raise DOMAIN (a, c)
   68.10        | SOME Ss => Ss);
   68.11      fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss);
    69.1 --- a/src/Pure/thm.ML	Thu Sep 15 17:16:55 2005 +0200
    69.2 +++ b/src/Pure/thm.ML	Thu Sep 15 17:16:56 2005 +0200
    69.3 @@ -526,7 +526,7 @@
    69.4  fun get_axiom_i theory name =
    69.5    let
    69.6      fun get_ax thy =
    69.7 -      Symtab.curried_lookup (#2 (#axioms (Theory.rep_theory thy))) name
    69.8 +      Symtab.lookup (#2 (#axioms (Theory.rep_theory thy))) name
    69.9        |> Option.map (fn prop =>
   69.10            Thm {thy_ref = Theory.self_ref thy,
   69.11              der = Pt.infer_derivs' I (false, Pt.axm_proof name prop),
   69.12 @@ -1484,7 +1484,7 @@
   69.13  fun invoke_oracle_i thy1 name =
   69.14    let
   69.15      val oracle =
   69.16 -      (case Symtab.curried_lookup (#2 (#oracles (Theory.rep_theory thy1))) name of
   69.17 +      (case Symtab.lookup (#2 (#oracles (Theory.rep_theory thy1))) name of
   69.18          NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
   69.19        | SOME (f, _) => f);
   69.20      val thy_ref1 = Theory.self_ref thy1;
    70.1 --- a/src/Pure/type.ML	Thu Sep 15 17:16:55 2005 +0200
    70.2 +++ b/src/Pure/type.ML	Thu Sep 15 17:16:56 2005 +0200
    70.3 @@ -167,7 +167,7 @@
    70.4              val Ts' = map cert Ts;
    70.5              fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
    70.6            in
    70.7 -            (case Symtab.curried_lookup types c of
    70.8 +            (case Symtab.lookup types c of
    70.9                SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
   70.10              | SOME (Abbreviation (vs, U, syn), _) => (nargs (length vs);
   70.11                  if syn then check_syntax c else ();
   70.12 @@ -284,7 +284,7 @@
   70.13    [TVar (ixn, S), TVar (ixn, S')], []);
   70.14  
   70.15  fun lookup (tye, (ixn, S)) =
   70.16 -  (case Vartab.curried_lookup tye ixn of
   70.17 +  (case Vartab.lookup tye ixn of
   70.18      NONE => NONE
   70.19    | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
   70.20  
   70.21 @@ -298,7 +298,7 @@
   70.22      fun match (TVar (v, S), T) subs =
   70.23            (case lookup (subs, (v, S)) of
   70.24              NONE =>
   70.25 -              if of_sort tsig (T, S) then Vartab.curried_update_new (v, (S, T)) subs
   70.26 +              if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs
   70.27                else raise TYPE_MATCH
   70.28            | SOME U => if U = T then subs else raise TYPE_MATCH)
   70.29        | match (Type (a, Ts), Type (b, Us)) subs =
   70.30 @@ -317,7 +317,7 @@
   70.31  (*purely structural matching*)
   70.32  fun raw_match (TVar (v, S), T) subs =
   70.33        (case lookup (subs, (v, S)) of
   70.34 -        NONE => Vartab.curried_update_new (v, (S, T)) subs
   70.35 +        NONE => Vartab.update_new (v, (S, T)) subs
   70.36        | SOME U => if U = T then subs else raise TYPE_MATCH)
   70.37    | raw_match (Type (a, Ts), Type (b, Us)) subs =
   70.38        if a <> b then raise TYPE_MATCH
   70.39 @@ -366,7 +366,7 @@
   70.40      fun meet (_, []) tye = tye
   70.41        | meet (TVar (xi, S'), S) tye =
   70.42            if Sorts.sort_le classes (S', S) then tye
   70.43 -          else Vartab.curried_update_new
   70.44 +          else Vartab.update_new
   70.45              (xi, (S', gen_tyvar (Sorts.inter_sort classes (S', S)))) tye
   70.46        | meet (TFree (_, S'), S) tye =
   70.47            if Sorts.sort_le classes (S', S) then tye
   70.48 @@ -381,19 +381,19 @@
   70.49            if eq_ix (v, w) then
   70.50              if S1 = S2 then tye else tvar_clash v S1 S2
   70.51            else if Sorts.sort_le classes (S1, S2) then
   70.52 -            Vartab.curried_update_new (w, (S2, T)) tye
   70.53 +            Vartab.update_new (w, (S2, T)) tye
   70.54            else if Sorts.sort_le classes (S2, S1) then
   70.55 -            Vartab.curried_update_new (v, (S1, U)) tye
   70.56 +            Vartab.update_new (v, (S1, U)) tye
   70.57            else
   70.58              let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in
   70.59 -              Vartab.curried_update_new (v, (S1, S)) (Vartab.curried_update_new (w, (S2, S)) tye)
   70.60 +              Vartab.update_new (v, (S1, S)) (Vartab.update_new (w, (S2, S)) tye)
   70.61              end
   70.62        | (TVar (v, S), T) =>
   70.63            if occurs v tye T then raise TUNIFY
   70.64 -          else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye)
   70.65 +          else meet (T, S) (Vartab.update_new (v, (S, T)) tye)
   70.66        | (T, TVar (v, S)) =>
   70.67            if occurs v tye T then raise TUNIFY
   70.68 -          else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye)
   70.69 +          else meet (T, S) (Vartab.update_new (v, (S, T)) tye)
   70.70        | (Type (a, Ts), Type (b, Us)) =>
   70.71            if a <> b then raise TUNIFY
   70.72            else unifs (Ts, Us) tye
   70.73 @@ -408,13 +408,13 @@
   70.74      (T as TVar (v, S1), U as TVar (w, S2)) =>
   70.75        if eq_ix (v, w) then
   70.76          if S1 = S2 then tye else tvar_clash v S1 S2
   70.77 -      else Vartab.curried_update_new (w, (S2, T)) tye
   70.78 +      else Vartab.update_new (w, (S2, T)) tye
   70.79    | (TVar (v, S), T) =>
   70.80        if occurs v tye T then raise TUNIFY
   70.81 -      else Vartab.curried_update_new (v, (S, T)) tye
   70.82 +      else Vartab.update_new (v, (S, T)) tye
   70.83    | (T, TVar (v, S)) =>
   70.84        if occurs v tye T then raise TUNIFY
   70.85 -      else Vartab.curried_update_new (v, (S, T)) tye
   70.86 +      else Vartab.update_new (v, (S, T)) tye
   70.87    | (Type (a, Ts), Type (b, Us)) =>
   70.88        if a <> b then raise TUNIFY
   70.89        else raw_unifys (Ts, Us) tye
   70.90 @@ -476,9 +476,9 @@
   70.91  
   70.92  fun insert_arities pp classes (t, ars) arities =
   70.93    let val ars' =
   70.94 -    Symtab.curried_lookup_multi arities t
   70.95 +    Symtab.lookup_multi arities t
   70.96      |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
   70.97 -  in Symtab.curried_update (t, ars') arities end;
   70.98 +  in Symtab.update (t, ars') arities end;
   70.99  
  70.100  fun insert_table pp classes = Symtab.fold (fn (t, ars) =>
  70.101    insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars));
  70.102 @@ -488,7 +488,7 @@
  70.103  fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
  70.104    let
  70.105      fun prep (t, Ss, S) =
  70.106 -      (case Symtab.curried_lookup (#2 types) t of
  70.107 +      (case Symtab.lookup (#2 types) t of
  70.108          SOME (LogicalType n, _) =>
  70.109            if length Ss = n then
  70.110              (t, map (cert_sort tsig) Ss, cert_sort tsig S)
  70.111 @@ -591,18 +591,18 @@
  70.112      val c' = NameSpace.full naming c;
  70.113      val space' = NameSpace.declare naming c' space;
  70.114      val types' =
  70.115 -      (case Symtab.curried_lookup types c' of
  70.116 +      (case Symtab.lookup types c' of
  70.117          SOME (decl', _) => err_in_decls c' decl decl'
  70.118 -      | NONE => Symtab.curried_update (c', (decl, stamp ())) types);
  70.119 +      | NONE => Symtab.update (c', (decl, stamp ())) types);
  70.120    in (space', types') end;
  70.121  
  70.122 -fun the_decl (_, types) = fst o the o Symtab.curried_lookup types;
  70.123 +fun the_decl (_, types) = fst o the o Symtab.lookup types;
  70.124  
  70.125  fun change_types f = map_tsig (fn (classes, default, types, arities) =>
  70.126    (classes, default, f types, arities));
  70.127  
  70.128  fun syntactic types (Type (c, Ts)) =
  70.129 -      (case Symtab.curried_lookup types c of SOME (Nonterminal, _) => true | _ => false)
  70.130 +      (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
  70.131          orelse exists (syntactic types) Ts
  70.132    | syntactic _ _ = false;
  70.133  
    71.1 --- a/src/ZF/Datatype.ML	Thu Sep 15 17:16:55 2005 +0200
    71.2 +++ b/src/ZF/Datatype.ML	Thu Sep 15 17:16:56 2005 +0200
    71.3 @@ -73,9 +73,9 @@
    71.4         and (rhead, rargs) = strip_comb rhs
    71.5         val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
    71.6         val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
    71.7 -       val lcon_info = the (Symtab.curried_lookup (ConstructorsData.get sg) lname)
    71.8 +       val lcon_info = the (Symtab.lookup (ConstructorsData.get sg) lname)
    71.9           handle Option => raise Match;
   71.10 -       val rcon_info = the (Symtab.curried_lookup (ConstructorsData.get sg) rname)
   71.11 +       val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname)
   71.12           handle Option => raise Match;
   71.13         val new = 
   71.14             if #big_rec_name lcon_info = #big_rec_name rcon_info 
    72.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Sep 15 17:16:55 2005 +0200
    72.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu Sep 15 17:16:56 2005 +0200
    72.3 @@ -383,8 +383,8 @@
    72.4            (("recursor_eqns", recursor_eqns), []),
    72.5            (("free_iffs", free_iffs), []),
    72.6            (("free_elims", free_SEs), [])])
    72.7 -        |> DatatypesData.map (Symtab.curried_update (big_rec_name, dt_info))
    72.8 -        |> ConstructorsData.map (fold Symtab.curried_update con_pairs)
    72.9 +        |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
   72.10 +        |> ConstructorsData.map (fold Symtab.update con_pairs)
   72.11          |> Theory.parent_path,
   72.12     ind_result,
   72.13     {con_defs = con_defs,
    73.1 --- a/src/ZF/Tools/ind_cases.ML	Thu Sep 15 17:16:55 2005 +0200
    73.2 +++ b/src/ZF/Tools/ind_cases.ML	Thu Sep 15 17:16:56 2005 +0200
    73.3 @@ -31,7 +31,7 @@
    73.4  end);
    73.5  
    73.6  
    73.7 -fun declare name f = IndCasesData.map (Symtab.curried_update (name, f));
    73.8 +fun declare name f = IndCasesData.map (Symtab.update (name, f));
    73.9  
   73.10  fun smart_cases thy ss read_prop s =
   73.11    let
   73.12 @@ -40,7 +40,7 @@
   73.13      val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
   73.14        (Logic.strip_imp_concl A)))))) handle TERM _ => err ();
   73.15    in
   73.16 -    (case Symtab.curried_lookup (IndCasesData.get thy) c of
   73.17 +    (case Symtab.lookup (IndCasesData.get thy) c of
   73.18        NONE => error ("Unknown inductive cases rule for set " ^ quote c)
   73.19      | SOME f => f ss (Thm.cterm_of (Theory.sign_of thy) A))
   73.20    end;
    74.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Sep 15 17:16:55 2005 +0200
    74.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Sep 15 17:16:56 2005 +0200
    74.3 @@ -70,7 +70,7 @@
    74.4  struct
    74.5  
    74.6  fun datatype_info thy name =
    74.7 -  (case Symtab.curried_lookup (DatatypesData.get thy) name of
    74.8 +  (case Symtab.lookup (DatatypesData.get thy) name of
    74.9      SOME info => info
   74.10    | NONE => error ("Unknown datatype " ^ quote name));
   74.11  
   74.12 @@ -166,8 +166,8 @@
   74.13      thy
   74.14      |> Theory.add_path (Sign.base_name big_rec_name)
   74.15      |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
   74.16 -    |> DatatypesData.put (Symtab.curried_update (big_rec_name, dt_info) (DatatypesData.get thy))
   74.17 -    |> ConstructorsData.put (fold_rev Symtab.curried_update con_pairs (ConstructorsData.get thy))
   74.18 +    |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   74.19 +    |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
   74.20      |> Theory.parent_path
   74.21    end;
   74.22  
    75.1 --- a/src/ZF/Tools/primrec_package.ML	Thu Sep 15 17:16:55 2005 +0200
    75.2 +++ b/src/ZF/Tools/primrec_package.ML	Thu Sep 15 17:16:56 2005 +0200
    75.3 @@ -56,7 +56,7 @@
    75.4        else strip_comb (hd middle);
    75.5      val (cname, _) = dest_Const constr
    75.6        handle TERM _ => raise RecError "ill-formed constructor";
    75.7 -    val con_info = the (Symtab.curried_lookup (ConstructorsData.get thy) cname)
    75.8 +    val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname)
    75.9        handle Option =>
   75.10        raise RecError "cannot determine datatype associated with function"
   75.11