curried_lookup/update;
authorwenzelm
Mon Sep 05 17:38:18 2005 +0200 (2005-09-05)
changeset 17261193b84a70ca4
parent 17260 df7c3b1f390a
child 17262 63cf42df2723
curried_lookup/update;
src/HOL/Import/hol4rews.ML
src/HOL/Matrix/cplex/CplexMatrixConverter.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/Pure/codegen.ML
src/ZF/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Mon Sep 05 17:38:17 2005 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Mon Sep 05 17:38:18 2005 +0200
     1.3 @@ -110,16 +110,12 @@
     1.4  structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs);
     1.5  
     1.6  fun get_segment2 thyname thy =
     1.7 -    let
     1.8 -	val imps = HOL4Imports.get thy
     1.9 -    in
    1.10 -	Symtab.lookup(imps,thyname)
    1.11 -    end
    1.12 +  Symtab.curried_lookup (HOL4Imports.get thy) thyname
    1.13  
    1.14  fun set_segment thyname segname thy =
    1.15      let
    1.16  	val imps = HOL4Imports.get thy
    1.17 -	val imps' = Symtab.update_new((thyname,segname),imps)
    1.18 +	val imps' = Symtab.curried_update_new (thyname,segname) imps
    1.19      in
    1.20  	HOL4Imports.put imps' thy
    1.21      end
    1.22 @@ -295,23 +291,19 @@
    1.23  fun add_hol4_move bef aft thy =
    1.24      let
    1.25  	val curmoves = HOL4Moves.get thy
    1.26 -	val newmoves = Symtab.update_new((bef,aft),curmoves)
    1.27 +	val newmoves = Symtab.curried_update_new (bef, aft) curmoves
    1.28      in
    1.29  	HOL4Moves.put newmoves thy
    1.30      end
    1.31  
    1.32  fun get_hol4_move bef thy =
    1.33 -    let
    1.34 -	val moves = HOL4Moves.get thy
    1.35 -    in
    1.36 -	Symtab.lookup(moves,bef)
    1.37 -    end
    1.38 +  Symtab.curried_lookup (HOL4Moves.get thy) bef
    1.39  
    1.40  fun follow_name thmname thy =
    1.41      let
    1.42  	val moves = HOL4Moves.get thy
    1.43  	fun F thmname =
    1.44 -	    case Symtab.lookup(moves,thmname) of
    1.45 +	    case Symtab.curried_lookup moves thmname of
    1.46  		SOME name => F name
    1.47  	      | NONE => thmname
    1.48      in
    1.49 @@ -321,23 +313,19 @@
    1.50  fun add_hol4_cmove bef aft thy =
    1.51      let
    1.52  	val curmoves = HOL4CMoves.get thy
    1.53 -	val newmoves = Symtab.update_new((bef,aft),curmoves)
    1.54 +	val newmoves = Symtab.curried_update_new (bef, aft) curmoves
    1.55      in
    1.56  	HOL4CMoves.put newmoves thy
    1.57      end
    1.58  
    1.59  fun get_hol4_cmove bef thy =
    1.60 -    let
    1.61 -	val moves = HOL4CMoves.get thy
    1.62 -    in
    1.63 -	Symtab.lookup(moves,bef)
    1.64 -    end
    1.65 +  Symtab.curried_lookup (HOL4CMoves.get thy) bef
    1.66  
    1.67  fun follow_cname thmname thy =
    1.68      let
    1.69  	val moves = HOL4CMoves.get thy
    1.70  	fun F thmname =
    1.71 -	    case Symtab.lookup(moves,thmname) of
    1.72 +	    case Symtab.curried_lookup moves thmname of
    1.73  		SOME name => F name
    1.74  	      | NONE => thmname
    1.75      in
     2.1 --- a/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Mon Sep 05 17:38:17 2005 +0200
     2.2 +++ b/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Mon Sep 05 17:38:18 2005 +0200
     2.3 @@ -57,14 +57,14 @@
     2.4      let	
     2.5  	fun build_naming index i2s s2i [] = (index, i2s, s2i)
     2.6  	  | build_naming index i2s s2i (cplexBounds (cplexNeg cplexInf, cplexLeq, cplexVar v, cplexLeq, cplexInf)::bounds)
     2.7 -	    = build_naming (index+1) (Inttab.update ((index, v), i2s)) (Symtab.update_new ((v, index), s2i)) bounds
     2.8 +	    = build_naming (index+1) (Inttab.curried_update (index, v) i2s) (Symtab.curried_update_new (v, index) s2i) bounds
     2.9  	  | build_naming _ _ _ _ = raise (Converter "nonfree bound")
    2.10  
    2.11  	val (varcount, i2s_tab, s2i_tab) = build_naming 0 Inttab.empty Symtab.empty bounds
    2.12  
    2.13 -	fun i2s i = case Inttab.lookup (i2s_tab, i) of NONE => raise (Converter "index not found")
    2.14 +	fun i2s i = case Inttab.curried_lookup i2s_tab i of NONE => raise (Converter "index not found")
    2.15  						     | SOME n => n
    2.16 -	fun s2i s = case Symtab.lookup (s2i_tab, s) of NONE => raise (Converter ("name not found: "^s))
    2.17 +	fun s2i s = case Symtab.curried_lookup s2i_tab s of NONE => raise (Converter ("name not found: "^s))
    2.18  						     | SOME i => i
    2.19  	fun num2str positive (cplexNeg t) = num2str (not positive) t
    2.20  	  | num2str positive (cplexNum num) = if positive then num else "-"^num			
     3.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Mon Sep 05 17:38:17 2005 +0200
     3.2 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Mon Sep 05 17:38:18 2005 +0200
     3.3 @@ -212,7 +212,7 @@
     3.4      else if (approx_value_term 1 I str) = zero_interval then 
     3.5  	vector
     3.6      else  
     3.7 -	Inttab.update ((index, str), vector)
     3.8 +	Inttab.curried_update (index, str) vector
     3.9  
    3.10  fun set_vector matrix index vector = 
    3.11      if index < 0 then
    3.12 @@ -220,7 +220,7 @@
    3.13      else if Inttab.is_empty vector then
    3.14  	matrix
    3.15      else
    3.16 -	Inttab.update ((index, vector), matrix)
    3.17 +	Inttab.curried_update (index, vector) matrix
    3.18  
    3.19  val empty_matrix = Inttab.empty
    3.20  val empty_vector = Inttab.empty
    3.21 @@ -232,9 +232,9 @@
    3.22  fun transpose_matrix matrix = 
    3.23      let
    3.24  	fun upd m j i x =
    3.25 -	    case Inttab.lookup (m, j) of
    3.26 -		SOME v => Inttab.update ((j, Inttab.update ((i, x), v)), m)
    3.27 -	      | NONE => Inttab.update ((j, Inttab.update ((i, x), Inttab.empty)), m) 
    3.28 +	    case Inttab.curried_lookup m j of
    3.29 +		SOME v => Inttab.curried_update (j, Inttab.curried_update (i, x) v) m
    3.30 +	      | NONE => Inttab.curried_update (j, Inttab.curried_update (i, x) Inttab.empty) m
    3.31  
    3.32  	fun updv j (m, (i, s)) = upd m i j s
    3.33  
    3.34 @@ -258,7 +258,7 @@
    3.35  	fun nameof i = 
    3.36  	    let 
    3.37  		val s = "x"^(Int.toString i)
    3.38 -		val _ = ytable := (Inttab.update ((i, s), !ytable))
    3.39 +		val _ = change ytable (Inttab.curried_update (i, s))
    3.40  	    in
    3.41  		s
    3.42  	    end
    3.43 @@ -281,7 +281,7 @@
    3.44  		       		       
    3.45  	fun mk_constr index vector c = 
    3.46  	    let 
    3.47 -		val s = case Inttab.lookup (c, index) of SOME s => s | NONE => "0"
    3.48 +		val s = case Inttab.curried_lookup c index of SOME s => s | NONE => "0"
    3.49  		val (p, s) = split_numstr s
    3.50  		val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
    3.51  	    in
    3.52 @@ -334,7 +334,7 @@
    3.53  		       		       
    3.54  	fun mk_constr index vector c = 
    3.55  	    let 
    3.56 -		val s = case Inttab.lookup (c, index) of SOME s => s | NONE => "0"
    3.57 +		val s = case Inttab.curried_lookup c index of SOME s => s | NONE => "0"
    3.58  		val (p, s) = split_numstr s
    3.59  		val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
    3.60  	    in
    3.61 @@ -358,7 +358,7 @@
    3.62  	val count = ref 0 
    3.63  	fun app (v, (i, s)) = 
    3.64  	    if (!count < size) then
    3.65 -		(count := !count +1 ; Inttab.update ((i,s),v))
    3.66 +		(count := !count +1 ; Inttab.curried_update (i,s) v)
    3.67  	    else
    3.68  		v
    3.69      in
    3.70 @@ -368,18 +368,18 @@
    3.71  fun cut_matrix vfilter vsize m = 
    3.72      let 
    3.73  	fun app (m, (i, v)) = 
    3.74 -	    if (Inttab.lookup (vfilter, i) = NONE) then 
    3.75 +	    if Inttab.curried_lookup vfilter i = NONE then 
    3.76  		m 
    3.77  	    else 
    3.78  		case vsize of
    3.79 -		    NONE => Inttab.update ((i,v), m)
    3.80 -		  | SOME s => Inttab.update((i, cut_vector s v),m)
    3.81 +		    NONE => Inttab.curried_update (i,v) m
    3.82 +		  | SOME s => Inttab.curried_update (i, cut_vector s v) m
    3.83      in
    3.84  	Inttab.foldl app (empty_matrix, m)
    3.85      end
    3.86  		 
    3.87 -fun v_elem_at v i = Inttab.lookup (v,i)
    3.88 -fun m_elem_at m i = Inttab.lookup (m,i)
    3.89 +fun v_elem_at v i = Inttab.curried_lookup v i
    3.90 +fun m_elem_at m i = Inttab.curried_lookup m i
    3.91  
    3.92  fun v_only_elem v = 
    3.93      case Inttab.min_key v of
     4.1 --- a/src/HOL/Matrix/cplex/fspmlp.ML	Mon Sep 05 17:38:17 2005 +0200
     4.2 +++ b/src/HOL/Matrix/cplex/fspmlp.ML	Mon Sep 05 17:38:18 2005 +0200
     4.3 @@ -54,11 +54,11 @@
     4.4      let 
     4.5  	val x = 
     4.6  	    case VarGraph.lookup (g, dest_key) of
     4.7 -		NONE => (NONE, Inttab.update ((row_index, (row_bound, [])), Inttab.empty))
     4.8 +		NONE => (NONE, Inttab.curried_update (row_index, (row_bound, [])) Inttab.empty)
     4.9  	      | SOME (sure_bound, f) =>
    4.10  		(sure_bound,
    4.11 -		 case Inttab.lookup (f, row_index) of
    4.12 -		     NONE => Inttab.update ((row_index, (row_bound, [])), f)
    4.13 +		 case Inttab.curried_lookup f row_index of
    4.14 +		     NONE => Inttab.curried_update (row_index, (row_bound, [])) f
    4.15  		   | SOME _ => raise (Internal "add_row_bound"))				     
    4.16      in
    4.17  	VarGraph.update ((dest_key, x), g)
    4.18 @@ -88,7 +88,7 @@
    4.19      case VarGraph.lookup (g, key) of
    4.20  	NONE => NONE
    4.21        | SOME (sure_bound, f) =>
    4.22 -	(case Inttab.lookup (f, row_index) of 
    4.23 +	(case Inttab.curried_lookup f row_index of 
    4.24  	     NONE => NONE
    4.25  	   | SOME (row_bound, _) => (sure_bound, row_bound))*)
    4.26      
    4.27 @@ -96,10 +96,10 @@
    4.28      case VarGraph.lookup (g, dest_key) of
    4.29  	NONE => raise (Internal "add_edge: dest_key not found")
    4.30        | SOME (sure_bound, f) =>
    4.31 -	(case Inttab.lookup (f, row_index) of
    4.32 +	(case Inttab.curried_lookup f row_index of
    4.33  	     NONE => raise (Internal "add_edge: row_index not found")
    4.34  	   | SOME (row_bound, sources) => 
    4.35 -	     VarGraph.update ((dest_key, (sure_bound, Inttab.update ((row_index, (row_bound, (coeff, src_key) :: sources)), f))), g))
    4.36 +	     VarGraph.curried_update (dest_key, (sure_bound, Inttab.curried_update (row_index, (row_bound, (coeff, src_key) :: sources)) f)) g)
    4.37  
    4.38  fun split_graph g = 
    4.39      let
    4.40 @@ -108,8 +108,8 @@
    4.41  		NONE => (r1, r2)
    4.42  	      | SOME bound => 
    4.43  		(case key of
    4.44 -		     (u, UPPER) => (r1, Inttab.update ((u, bound), r2))
    4.45 -		   | (u, LOWER) => (Inttab.update ((u, bound), r1), r2))
    4.46 +		     (u, UPPER) => (r1, Inttab.curried_update (u, bound) r2)
    4.47 +		   | (u, LOWER) => (Inttab.curried_update (u, bound) r1, r2))
    4.48      in
    4.49  	VarGraph.foldl split ((Inttab.empty, Inttab.empty), g)
    4.50      end
    4.51 @@ -195,7 +195,7 @@
    4.52      let
    4.53  	val empty = Inttab.empty
    4.54  
    4.55 -	fun instab t i x = Inttab.update ((i,x), t)
    4.56 +	fun instab t i x = Inttab.curried_update (i, x) t
    4.57  
    4.58  	fun isnegstr x = String.isPrefix "-" x
    4.59  	fun negstr x = if isnegstr x then String.extract (x, 1, NONE) else "-"^x
    4.60 @@ -280,8 +280,8 @@
    4.61  		let
    4.62  		    val index = xlen-i
    4.63  		    val (r, (r12_1, r12_2)) = abs_estimate (i-1) r1 r2 
    4.64 -		    val b1 = case Inttab.lookup (r1, index) of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x
    4.65 -		    val b2 = case Inttab.lookup (r2, index) of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x
    4.66 +		    val b1 = case Inttab.curried_lookup r1 index of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x
    4.67 +		    val b2 = case Inttab.curried_lookup r2 index of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x
    4.68  		    val abs_max = FloatArith.max (FloatArith.neg (FloatArith.negative_part b1)) (FloatArith.positive_part b2)    
    4.69  		in
    4.70  		    (add_row_entry r index abs_max, (add_row_entry r12_1 index b1, add_row_entry r12_2 index b2))
     5.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Sep 05 17:38:17 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Sep 05 17:38:18 2005 +0200
     5.3 @@ -57,15 +57,14 @@
     5.4  
     5.5  fun axioms_having_consts_aux [] tab thms = thms
     5.6    | axioms_having_consts_aux (c::cs) tab thms =
     5.7 -    let val thms1 = Symtab.lookup(tab,c)
     5.8 -	val thms2 = 
     5.9 -	    case thms1 of (SOME x) => x
    5.10 -			| NONE => []
    5.11 +    let val thms1 = Symtab.curried_lookup tab c
    5.12 +      val thms2 = 
    5.13 +          case thms1 of (SOME x) => x
    5.14 +                      | NONE => []
    5.15      in
    5.16 -	axioms_having_consts_aux cs tab (thms2 union thms)
    5.17 +      axioms_having_consts_aux cs tab (thms2 union thms)
    5.18      end;
    5.19  
    5.20 -
    5.21  fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab [];
    5.22  
    5.23  
     6.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Sep 05 17:38:17 2005 +0200
     6.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Sep 05 17:38:18 2005 +0200
     6.3 @@ -168,7 +168,7 @@
     6.4  
     6.5          val inject = map (fn r => r RS iffD1)
     6.6            (if i < length newTs then List.nth (constr_inject, i)
     6.7 -            else #inject (valOf (Symtab.lookup (dt_info, tname))));
     6.8 +            else #inject (the (Symtab.curried_lookup dt_info tname)));
     6.9  
    6.10          fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
    6.11            let
     7.1 --- a/src/HOL/Tools/datatype_aux.ML	Mon Sep 05 17:38:17 2005 +0200
     7.2 +++ b/src/HOL/Tools/datatype_aux.ML	Mon Sep 05 17:38:18 2005 +0200
     7.3 @@ -299,7 +299,7 @@
     7.4        Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
     7.5  
     7.6      fun get_dt_descr T i tname dts =
     7.7 -      (case Symtab.lookup (dt_info, tname) of
     7.8 +      (case Symtab.curried_lookup dt_info tname of
     7.9           NONE => typ_error T (tname ^ " is not a datatype - can't use it in\
    7.10             \ nested recursion")
    7.11         | (SOME {index, descr, ...}) =>
     8.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Sep 05 17:38:17 2005 +0200
     8.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Sep 05 17:38:18 2005 +0200
     8.3 @@ -281,7 +281,7 @@
     8.4   |  _ => NONE);
     8.5  
     8.6  fun datatype_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
     8.7 -      (case Symtab.lookup (DatatypePackage.get_datatypes thy, s) of
     8.8 +      (case Symtab.curried_lookup (DatatypePackage.get_datatypes thy) s of
     8.9           NONE => NONE
    8.10         | SOME {descr, ...} =>
    8.11             if isSome (get_assoc_type thy s) then NONE else
     9.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Sep 05 17:38:17 2005 +0200
     9.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Sep 05 17:38:18 2005 +0200
     9.3 @@ -104,7 +104,7 @@
     9.4  
     9.5  (** theory information about datatypes **)
     9.6  
     9.7 -fun datatype_info thy name = Symtab.lookup (get_datatypes thy, name);
     9.8 +val datatype_info = Symtab.curried_lookup o get_datatypes;
     9.9  
    9.10  fun datatype_info_err thy name = (case datatype_info thy name of
    9.11        SOME info => info
    9.12 @@ -681,7 +681,7 @@
    9.13        Theory.add_path (space_implode "_" new_type_names) |>
    9.14        add_rules simps case_thms size_thms rec_thms inject distinct
    9.15                  weak_case_congs Simplifier.cong_add_global |> 
    9.16 -      put_datatypes (foldr Symtab.update dt_info dt_infos) |>
    9.17 +      put_datatypes (fold Symtab.curried_update dt_infos dt_info) |>
    9.18        add_cases_induct dt_infos induct |>
    9.19        Theory.parent_path |>
    9.20        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    9.21 @@ -739,7 +739,7 @@
    9.22        Theory.add_path (space_implode "_" new_type_names) |>
    9.23        add_rules simps case_thms size_thms rec_thms inject distinct
    9.24                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
    9.25 -      put_datatypes (foldr Symtab.update dt_info dt_infos) |>
    9.26 +      put_datatypes (fold Symtab.curried_update dt_infos dt_info) |>
    9.27        add_cases_induct dt_infos induct |>
    9.28        Theory.parent_path |>
    9.29        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    9.30 @@ -847,7 +847,7 @@
    9.31        Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
    9.32        add_rules simps case_thms size_thms rec_thms inject distinct
    9.33                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
    9.34 -      put_datatypes (foldr Symtab.update dt_info dt_infos) |>
    9.35 +      put_datatypes (fold Symtab.curried_update dt_infos dt_info) |>
    9.36        add_cases_induct dt_infos induction' |>
    9.37        Theory.parent_path |>
    9.38        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    10.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Sep 05 17:38:17 2005 +0200
    10.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Sep 05 17:38:18 2005 +0200
    10.3 @@ -35,7 +35,7 @@
    10.4  
    10.5  
    10.6  fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
    10.7 -  #exhaustion (valOf (Symtab.lookup (dt_info, tname)));
    10.8 +  #exhaustion (the (Symtab.curried_lookup dt_info tname));
    10.9  
   10.10  (******************************************************************************)
   10.11  
   10.12 @@ -356,7 +356,7 @@
   10.13        let
   10.14          val ks = map fst ds;
   10.15          val (_, (tname, _, _)) = hd ds;
   10.16 -        val {rec_rewrites, rec_names, ...} = valOf (Symtab.lookup (dt_info, tname));
   10.17 +        val {rec_rewrites, rec_names, ...} = the (Symtab.curried_lookup dt_info tname);
   10.18  
   10.19          fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) =
   10.20            let
   10.21 @@ -412,7 +412,7 @@
   10.22      fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
   10.23        let
   10.24          val (_, (tname, _, _)) = hd ds;
   10.25 -        val {induction, ...} = valOf (Symtab.lookup (dt_info, tname));
   10.26 +        val {induction, ...} = the (Symtab.curried_lookup dt_info tname);
   10.27  
   10.28          fun mk_ind_concl (i, _) =
   10.29            let
    11.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Sep 05 17:38:17 2005 +0200
    11.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Sep 05 17:38:18 2005 +0200
    11.3 @@ -55,9 +55,8 @@
    11.4          Const (s, _) =>
    11.5            let val cs = foldr add_term_consts [] (prems_of thm)
    11.6            in (CodegenData.put
    11.7 -            {intros = Symtab.update ((s,
    11.8 -               getOpt (Symtab.lookup (intros, s), []) @
    11.9 -                 [(thm, thyname_of s)]), intros),
   11.10 +            {intros = intros |>
   11.11 +             Symtab.curried_update (s, Symtab.curried_lookup_multi intros s @ [(thm, thyname_of s)]),
   11.12               graph = foldr (uncurry (Graph.add_edge o pair s))
   11.13                 (Library.foldl add_node (graph, s :: cs)) cs,
   11.14               eqns = eqns} thy, thm)
   11.15 @@ -66,16 +65,15 @@
   11.16      | _ $ (Const ("op =", _) $ t $ _) => (case head_of t of
   11.17          Const (s, _) =>
   11.18            (CodegenData.put {intros = intros, graph = graph,
   11.19 -             eqns = Symtab.update ((s,
   11.20 -               getOpt (Symtab.lookup (eqns, s), []) @
   11.21 -                 [(thm, thyname_of s)]), eqns)} thy, thm)
   11.22 +             eqns = eqns |> Symtab.curried_update
   11.23 +               (s, Symtab.curried_lookup_multi eqns s @ [(thm, thyname_of s)])} thy, thm)
   11.24        | _ => (warn thm; p))
   11.25      | _ => (warn thm; p))
   11.26    end;
   11.27  
   11.28  fun get_clauses thy s =
   11.29    let val {intros, graph, ...} = CodegenData.get thy
   11.30 -  in case Symtab.lookup (intros, s) of
   11.31 +  in case Symtab.curried_lookup intros s of
   11.32        NONE => (case InductivePackage.get_inductive thy s of
   11.33          NONE => NONE
   11.34        | SOME ({names, ...}, {intrs, ...}) =>
   11.35 @@ -86,7 +84,7 @@
   11.36            val SOME names = find_first
   11.37              (fn xs => s mem xs) (Graph.strong_conn graph);
   11.38            val intrs = List.concat (map
   11.39 -            (fn s => valOf (Symtab.lookup (intros, s))) names);
   11.40 +            (fn s => the (Symtab.curried_lookup intros s)) names);
   11.41            val (_, (_, thyname)) = split_last intrs
   11.42          in SOME (names, thyname, preprocess thy (map fst intrs)) end
   11.43    end;
   11.44 @@ -718,7 +716,7 @@
   11.45             (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
   11.46          handle TERM _ => mk_ind_call thy defs gr dep module t u true)
   11.47    | inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
   11.48 -      (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy), s) of
   11.49 +      (Const (s, _), ts) => (case Symtab.curried_lookup (#eqns (CodegenData.get thy)) s of
   11.50          NONE => list_of_indset thy defs gr dep module brack t
   11.51        | SOME eqns =>
   11.52            let
    12.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Sep 05 17:38:17 2005 +0200
    12.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Sep 05 17:38:18 2005 +0200
    12.3 @@ -112,7 +112,7 @@
    12.4  
    12.5  (* get and put data *)
    12.6  
    12.7 -fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
    12.8 +val get_inductive = Symtab.curried_lookup o #1 o InductiveData.get;
    12.9  
   12.10  fun the_inductive thy name =
   12.11    (case get_inductive thy name of
   12.12 @@ -123,7 +123,7 @@
   12.13  
   12.14  fun put_inductives names info thy =
   12.15    let
   12.16 -    fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
   12.17 +    fun upd ((tab, monos), name) = (Symtab.curried_update_new (name, info) tab, monos);
   12.18      val tab_monos = Library.foldl upd (InductiveData.get thy, names)
   12.19        handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
   12.20    in InductiveData.put tab_monos thy end;
    13.1 --- a/src/HOL/Tools/primrec_package.ML	Mon Sep 05 17:38:17 2005 +0200
    13.2 +++ b/src/HOL/Tools/primrec_package.ML	Mon Sep 05 17:38:18 2005 +0200
    13.3 @@ -205,7 +205,7 @@
    13.4  
    13.5  fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
    13.6    | find_dts dt_info tnames' (tname::tnames) =
    13.7 -      (case Symtab.lookup (dt_info, tname) of
    13.8 +      (case Symtab.curried_lookup dt_info tname of
    13.9            NONE => primrec_err (quote tname ^ " is not a datatype")
   13.10          | SOME dt =>
   13.11              if tnames' subset (map (#1 o snd) (#descr dt)) then
    14.1 --- a/src/HOL/Tools/recdef_package.ML	Mon Sep 05 17:38:17 2005 +0200
    14.2 +++ b/src/HOL/Tools/recdef_package.ML	Mon Sep 05 17:38:18 2005 +0200
    14.3 @@ -127,12 +127,12 @@
    14.4  val print_recdefs = GlobalRecdefData.print;
    14.5  
    14.6  
    14.7 -fun get_recdef thy name = Symtab.lookup (#1 (GlobalRecdefData.get thy), name);
    14.8 +val get_recdef = Symtab.curried_lookup o #1 o GlobalRecdefData.get;
    14.9  
   14.10  fun put_recdef name info thy =
   14.11    let
   14.12      val (tab, hints) = GlobalRecdefData.get thy;
   14.13 -    val tab' = Symtab.update_new ((name, info), tab)
   14.14 +    val tab' = Symtab.curried_update_new (name, info) tab
   14.15        handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
   14.16    in GlobalRecdefData.put (tab', hints) thy end;
   14.17  
    15.1 --- a/src/HOL/Tools/recfun_codegen.ML	Mon Sep 05 17:38:17 2005 +0200
    15.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Mon Sep 05 17:38:18 2005 +0200
    15.3 @@ -42,8 +42,7 @@
    15.4      val (s, _) = const_of (prop_of thm);
    15.5    in
    15.6      if Pattern.pattern (lhs_of thm) then
    15.7 -      (CodegenData.put (Symtab.update ((s,
    15.8 -        (thm, optmod) :: getOpt (Symtab.lookup (tab, s), [])), tab)) thy, thm)
    15.9 +      (CodegenData.put (Symtab.curried_update_multi (s, (thm, optmod)) tab) thy, thm)
   15.10      else (warn thm; p)
   15.11    end handle TERM _ => (warn thm; p);
   15.12  
   15.13 @@ -51,10 +50,10 @@
   15.14    let
   15.15      val tab = CodegenData.get thy;
   15.16      val (s, _) = const_of (prop_of thm);
   15.17 -  in case Symtab.lookup (tab, s) of
   15.18 +  in case Symtab.curried_lookup tab s of
   15.19        NONE => p
   15.20 -    | SOME thms => (CodegenData.put (Symtab.update ((s,
   15.21 -        gen_rem (eq_thm o apfst fst) (thms, thm)), tab)) thy, thm)
   15.22 +    | SOME thms => (CodegenData.put (Symtab.curried_update (s,
   15.23 +        gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy, thm)
   15.24    end handle TERM _ => (warn thm; p);
   15.25  
   15.26  fun del_redundant thy eqs [] = eqs
   15.27 @@ -65,7 +64,7 @@
   15.28      in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
   15.29  
   15.30  fun get_equations thy defs (s, T) =
   15.31 -  (case Symtab.lookup (CodegenData.get thy, s) of
   15.32 +  (case Symtab.curried_lookup (CodegenData.get thy) s of
   15.33       NONE => ([], "")
   15.34     | SOME thms => 
   15.35         let val thms' = del_redundant thy []
    16.1 --- a/src/HOL/Tools/record_package.ML	Mon Sep 05 17:38:17 2005 +0200
    16.2 +++ b/src/HOL/Tools/record_package.ML	Mon Sep 05 17:38:18 2005 +0200
    16.3 @@ -17,7 +17,7 @@
    16.4    val record_split_name: string
    16.5    val record_split_wrapper: string * wrapper
    16.6    val print_record_type_abbr: bool ref
    16.7 -  val print_record_type_as_fields: bool ref 
    16.8 +  val print_record_type_as_fields: bool ref
    16.9  end;
   16.10  
   16.11  signature RECORD_PACKAGE =
   16.12 @@ -43,7 +43,7 @@
   16.13  end;
   16.14  
   16.15  
   16.16 -structure RecordPackage:RECORD_PACKAGE =     
   16.17 +structure RecordPackage:RECORD_PACKAGE =
   16.18  struct
   16.19  
   16.20  val rec_UNIV_I = thm "rec_UNIV_I";
   16.21 @@ -63,7 +63,7 @@
   16.22  val wN = "w";
   16.23  val moreN = "more";
   16.24  val schemeN = "_scheme";
   16.25 -val ext_typeN = "_ext_type"; 
   16.26 +val ext_typeN = "_ext_type";
   16.27  val extN ="_ext";
   16.28  val casesN = "_cases";
   16.29  val ext_dest = "_sel";
   16.30 @@ -94,7 +94,7 @@
   16.31  
   16.32  fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
   16.33  fun timing_msg s = if !timing then warning s else ();
   16.34 - 
   16.35 +
   16.36  (* syntax *)
   16.37  
   16.38  fun prune n xs = Library.drop (n, xs);
   16.39 @@ -136,9 +136,9 @@
   16.40  fun mk_casesC (name,T,vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT)
   16.41  
   16.42  fun mk_cases (name,T,vT) f =
   16.43 -  let val Ts = binder_types (fastype_of f) 
   16.44 +  let val Ts = binder_types (fastype_of f)
   16.45    in Const (mk_casesC (name,T,vT) Ts) $ f end;
   16.46 - 
   16.47 +
   16.48  (* selector *)
   16.49  
   16.50  fun mk_selC sT (c,T) = (c,sT --> T);
   16.51 @@ -165,7 +165,7 @@
   16.52    | dest_recT typ = raise TYPE ("RecordPackage.dest_recT", [typ], []);
   16.53  
   16.54  fun is_recT T =
   16.55 -  (case try dest_recT T of NONE => false | SOME _ => true); 
   16.56 +  (case try dest_recT T of NONE => false | SOME _ => true);
   16.57  
   16.58  fun dest_recTs T =
   16.59    let val ((c, Ts), U) = dest_recT T
   16.60 @@ -179,7 +179,7 @@
   16.61        | SOME l => SOME l)
   16.62    end handle TYPE _ => NONE
   16.63  
   16.64 -fun rec_id i T = 
   16.65 +fun rec_id i T =
   16.66    let val rTs = dest_recTs T
   16.67        val rTs' = if i < 0 then rTs else Library.take (i,rTs)
   16.68    in Library.foldl (fn (s,(c,T)) => s ^ c) ("",rTs') end;
   16.69 @@ -199,7 +199,7 @@
   16.70   };
   16.71  
   16.72  fun make_record_info args parent fields extension induct =
   16.73 - {args = args, parent = parent, fields = fields, extension = extension, 
   16.74 + {args = args, parent = parent, fields = fields, extension = extension,
   16.75    induct = induct}: record_info;
   16.76  
   16.77  
   16.78 @@ -224,20 +224,20 @@
   16.79    equalities: thm Symtab.table,
   16.80    extinjects: thm list,
   16.81    extsplit: thm Symtab.table, (* maps extension name to split rule *)
   16.82 -  splits: (thm*thm*thm*thm) Symtab.table,    (* !!,!,EX - split-equalities,induct rule *) 
   16.83 +  splits: (thm*thm*thm*thm) Symtab.table,    (* !!,!,EX - split-equalities,induct rule *)
   16.84    extfields: (string*typ) list Symtab.table, (* maps extension to its fields *)
   16.85    fieldext: (string*typ list) Symtab.table   (* maps field to its extension *)
   16.86  };
   16.87  
   16.88 -fun make_record_data 
   16.89 +fun make_record_data
   16.90        records sel_upd equalities extinjects extsplit splits extfields fieldext =
   16.91 - {records = records, sel_upd = sel_upd, 
   16.92 -  equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, 
   16.93 + {records = records, sel_upd = sel_upd,
   16.94 +  equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
   16.95    extfields = extfields, fieldext = fieldext }: record_data;
   16.96  
   16.97  structure RecordsData = TheoryDataFun
   16.98  (struct
   16.99 -  val name = "HOL/records";       
  16.100 +  val name = "HOL/records";
  16.101    type T = record_data;
  16.102  
  16.103    val empty =
  16.104 @@ -251,7 +251,7 @@
  16.105     ({records = recs1,
  16.106       sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
  16.107       equalities = equalities1,
  16.108 -     extinjects = extinjects1, 
  16.109 +     extinjects = extinjects1,
  16.110       extsplit = extsplit1,
  16.111       splits = splits1,
  16.112       extfields = extfields1,
  16.113 @@ -259,12 +259,12 @@
  16.114      {records = recs2,
  16.115       sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
  16.116       equalities = equalities2,
  16.117 -     extinjects = extinjects2, 
  16.118 -     extsplit = extsplit2, 
  16.119 +     extinjects = extinjects2,
  16.120 +     extsplit = extsplit2,
  16.121       splits = splits2,
  16.122       extfields = extfields2,
  16.123       fieldext = fieldext2}) =
  16.124 -    make_record_data  
  16.125 +    make_record_data
  16.126        (Symtab.merge (K true) (recs1, recs2))
  16.127        {selectors = Symtab.merge (K true) (sels1, sels2),
  16.128          updates = Symtab.merge (K true) (upds1, upds2),
  16.129 @@ -272,9 +272,9 @@
  16.130        (Symtab.merge Thm.eq_thm (equalities1, equalities2))
  16.131        (gen_merge_lists Thm.eq_thm extinjects1 extinjects2)
  16.132        (Symtab.merge Thm.eq_thm (extsplit1,extsplit2))
  16.133 -      (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) 
  16.134 -                     => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso 
  16.135 -                        Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) 
  16.136 +      (Symtab.merge (fn ((a,b,c,d),(w,x,y,z))
  16.137 +                     => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso
  16.138 +                        Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z))
  16.139                      (splits1, splits2))
  16.140        (Symtab.merge (K true) (extfields1,extfields2))
  16.141        (Symtab.merge (K true) (fieldext1,fieldext2));
  16.142 @@ -303,13 +303,13 @@
  16.143  
  16.144  (* access 'records' *)
  16.145  
  16.146 -fun get_record thy name = Symtab.lookup (#records (RecordsData.get thy), name);
  16.147 +val get_record = Symtab.curried_lookup o #records o RecordsData.get;
  16.148  
  16.149  fun put_record name info thy =
  16.150    let
  16.151 -    val {records, sel_upd, equalities, extinjects,extsplit,splits,extfields,fieldext} = 
  16.152 +    val {records, sel_upd, equalities, extinjects,extsplit,splits,extfields,fieldext} =
  16.153            RecordsData.get thy;
  16.154 -    val data = make_record_data (Symtab.update ((name, info), records))
  16.155 +    val data = make_record_data (Symtab.curried_update (name, info) records)
  16.156        sel_upd equalities extinjects extsplit splits extfields fieldext;
  16.157    in RecordsData.put data thy end;
  16.158  
  16.159 @@ -317,22 +317,18 @@
  16.160  
  16.161  val get_sel_upd = #sel_upd o RecordsData.get;
  16.162  
  16.163 -fun get_selectors sg name = Symtab.lookup (#selectors (get_sel_upd sg), name);
  16.164 -fun is_selector sg name = 
  16.165 -  case get_selectors sg (Sign.intern_const sg name) of 
  16.166 -     NONE => false
  16.167 -   | SOME _ => true
  16.168 +val get_selectors = Symtab.curried_lookup o #selectors o get_sel_upd;
  16.169 +fun is_selector sg name = is_some (get_selectors sg (Sign.intern_const sg name));
  16.170  
  16.171 -                             
  16.172 -fun get_updates sg name = Symtab.lookup (#updates (get_sel_upd sg), name);
  16.173 -fun get_simpset sg = #simpset (get_sel_upd sg);
  16.174 +val get_updates = Symtab.curried_lookup o #updates o get_sel_upd;
  16.175 +val get_simpset = #simpset o get_sel_upd;
  16.176  
  16.177  fun put_sel_upd names simps thy =
  16.178    let
  16.179      val sels = map (rpair ()) names;
  16.180      val upds = map (suffix updateN) names ~~ names;
  16.181  
  16.182 -    val {records, sel_upd = {selectors, updates, simpset}, 
  16.183 +    val {records, sel_upd = {selectors, updates, simpset},
  16.184        equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy;
  16.185      val data = make_record_data records
  16.186        {selectors = Symtab.extend (selectors, sels),
  16.187 @@ -345,23 +341,22 @@
  16.188  
  16.189  fun add_record_equalities name thm thy =
  16.190    let
  16.191 -    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = 
  16.192 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
  16.193            RecordsData.get thy;
  16.194 -    val data = make_record_data records sel_upd 
  16.195 -           (Symtab.update_new ((name, thm), equalities)) extinjects extsplit 
  16.196 +    val data = make_record_data records sel_upd
  16.197 +           (Symtab.curried_update_new (name, thm) equalities) extinjects extsplit
  16.198             splits extfields fieldext;
  16.199    in RecordsData.put data thy end;
  16.200  
  16.201 -fun get_equalities sg name =
  16.202 -  Symtab.lookup (#equalities (RecordsData.get sg), name);
  16.203 +val get_equalities =Symtab.curried_lookup o #equalities o RecordsData.get;
  16.204  
  16.205  (* access 'extinjects' *)
  16.206  
  16.207  fun add_extinjects thm thy =
  16.208    let
  16.209 -    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = 
  16.210 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
  16.211            RecordsData.get thy;
  16.212 -    val data = make_record_data records sel_upd equalities (extinjects@[thm]) extsplit  
  16.213 +    val data = make_record_data records sel_upd equalities (extinjects@[thm]) extsplit
  16.214                   splits extfields fieldext;
  16.215    in RecordsData.put data thy end;
  16.216  
  16.217 @@ -371,73 +366,69 @@
  16.218  
  16.219  fun add_extsplit name thm thy =
  16.220    let
  16.221 -    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = 
  16.222 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
  16.223            RecordsData.get thy;
  16.224 -    val data = make_record_data records sel_upd 
  16.225 -      equalities extinjects (Symtab.update_new ((name, thm), extsplit)) splits 
  16.226 +    val data = make_record_data records sel_upd
  16.227 +      equalities extinjects (Symtab.curried_update_new (name, thm) extsplit) splits
  16.228        extfields fieldext;
  16.229    in RecordsData.put data thy end;
  16.230  
  16.231 -fun get_extsplit sg name =
  16.232 -  Symtab.lookup (#extsplit (RecordsData.get sg), name);
  16.233 +val get_extsplit = Symtab.curried_lookup o #extsplit o RecordsData.get;
  16.234  
  16.235  (* access 'splits' *)
  16.236  
  16.237  fun add_record_splits name thmP thy =
  16.238    let
  16.239 -    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = 
  16.240 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
  16.241            RecordsData.get thy;
  16.242 -    val data = make_record_data records sel_upd 
  16.243 -      equalities extinjects extsplit (Symtab.update_new ((name, thmP), splits)) 
  16.244 +    val data = make_record_data records sel_upd
  16.245 +      equalities extinjects extsplit (Symtab.curried_update_new (name, thmP) splits)
  16.246        extfields fieldext;
  16.247    in RecordsData.put data thy end;
  16.248  
  16.249 -fun get_splits sg name =
  16.250 -  Symtab.lookup (#splits (RecordsData.get sg), name);
  16.251 +val get_splits = Symtab.curried_lookup o #splits o RecordsData.get;
  16.252  
  16.253  
  16.254  
  16.255  (* extension of a record name *)
  16.256 -fun get_extension sg name =
  16.257 - case Symtab.lookup (#records (RecordsData.get sg),name) of
  16.258 -        SOME s => SOME (#extension s)
  16.259 -      | NONE => NONE;
  16.260 +val get_extension =
  16.261 +  Option.map #extension oo (Symtab.curried_lookup o #records o RecordsData.get);
  16.262 +
  16.263  
  16.264  (* access 'extfields' *)
  16.265  
  16.266  fun add_extfields name fields thy =
  16.267    let
  16.268 -    val {records, sel_upd, equalities, extinjects, extsplit,splits, extfields, fieldext} = 
  16.269 +    val {records, sel_upd, equalities, extinjects, extsplit,splits, extfields, fieldext} =
  16.270            RecordsData.get thy;
  16.271 -    val data = make_record_data records sel_upd 
  16.272 -         equalities extinjects extsplit splits 
  16.273 -         (Symtab.update_new ((name, fields), extfields)) fieldext;
  16.274 +    val data = make_record_data records sel_upd
  16.275 +         equalities extinjects extsplit splits
  16.276 +         (Symtab.curried_update_new (name, fields) extfields) fieldext;
  16.277    in RecordsData.put data thy end;
  16.278  
  16.279 -fun get_extfields sg name =
  16.280 -  Symtab.lookup (#extfields (RecordsData.get sg), name);
  16.281 +val get_extfields = Symtab.curried_lookup o #extfields o RecordsData.get;
  16.282  
  16.283 -fun get_extT_fields sg T = 
  16.284 +fun get_extT_fields sg T =
  16.285    let
  16.286      val ((name,Ts),moreT) = dest_recT T;
  16.287 -    val recname = let val (nm::recn::rst) = rev (NameSpace.unpack name) 
  16.288 +    val recname = let val (nm::recn::rst) = rev (NameSpace.unpack name)
  16.289                    in NameSpace.pack (rev (nm::rst)) end;
  16.290      val midx = maxidx_of_typs (moreT::Ts);
  16.291      fun varify (a, S) = TVar ((a, midx), S);
  16.292      val varifyT = map_type_tfree varify;
  16.293      val {records,extfields,...} = RecordsData.get sg;
  16.294 -    val (flds,(more,_)) = split_last (Symtab.lookup_multi (extfields,name));
  16.295 -    val args = map varifyT (snd (#extension (valOf (Symtab.lookup (records,recname)))));
  16.296 +    val (flds,(more,_)) = split_last (Symtab.curried_lookup_multi extfields name);
  16.297 +    val args = map varifyT (snd (#extension (the (Symtab.curried_lookup records recname))));
  16.298  
  16.299      val (subst,_) = fold (Sign.typ_unify sg) (but_last args ~~ but_last Ts) (Vartab.empty,0);
  16.300      val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds;
  16.301    in (flds',(more,moreT)) end;
  16.302  
  16.303 -fun get_recT_fields sg T = 
  16.304 -  let 
  16.305 +fun get_recT_fields sg T =
  16.306 +  let
  16.307      val (root_flds,(root_more,root_moreT)) = get_extT_fields sg T;
  16.308 -    val (rest_flds,rest_more) = 
  16.309 -	   if is_recT root_moreT then get_recT_fields sg root_moreT 
  16.310 +    val (rest_flds,rest_more) =
  16.311 +           if is_recT root_moreT then get_recT_fields sg root_moreT
  16.312             else ([],(root_more,root_moreT));
  16.313    in (root_flds@rest_flds,rest_more) end;
  16.314  
  16.315 @@ -446,17 +437,16 @@
  16.316  
  16.317  fun add_fieldext extname_types fields thy =
  16.318    let
  16.319 -    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = 
  16.320 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
  16.321             RecordsData.get thy;
  16.322 -    val fieldext' = Library.foldl (fn (table,field) => Symtab.update_new ((field,extname_types),table))  
  16.323 -                          (fieldext,fields);
  16.324 -    val data=make_record_data records sel_upd equalities extinjects extsplit 
  16.325 +    val fieldext' =
  16.326 +      fold (fn field => Symtab.curried_update_new (field, extname_types)) fields fieldext;
  16.327 +    val data=make_record_data records sel_upd equalities extinjects extsplit
  16.328                splits extfields fieldext';
  16.329    in RecordsData.put data thy end;
  16.330  
  16.331  
  16.332 -fun get_fieldext sg name =
  16.333 -  Symtab.lookup (#fieldext (RecordsData.get sg), name);
  16.334 +val get_fieldext = Symtab.curried_lookup o #fieldext o RecordsData.get;
  16.335  
  16.336  (* parent records *)
  16.337  
  16.338 @@ -522,9 +512,9 @@
  16.339    | dest_ext_fields _ mark t = [dest_ext_field mark t]
  16.340  
  16.341  fun gen_ext_fields_tr sep mark sfx more sg t =
  16.342 -  let 
  16.343 +  let
  16.344      val msg = "error in record input: ";
  16.345 -    val fieldargs = dest_ext_fields sep mark t; 
  16.346 +    val fieldargs = dest_ext_fields sep mark t;
  16.347      fun splitargs (field::fields) ((name,arg)::fargs) =
  16.348            if can (unsuffix name) field
  16.349            then let val (args,rest) = splitargs fields fargs
  16.350 @@ -537,10 +527,10 @@
  16.351      fun mk_ext (fargs as (name,arg)::_) =
  16.352           (case get_fieldext sg (Sign.intern_const sg name) of
  16.353              SOME (ext,_) => (case get_extfields sg ext of
  16.354 -                               SOME flds 
  16.355 -                                 => let val (args,rest) = 
  16.356 +                               SOME flds
  16.357 +                                 => let val (args,rest) =
  16.358                                                 splitargs (map fst (but_last flds)) fargs;
  16.359 -                                        val more' = mk_ext rest;  
  16.360 +                                        val more' = mk_ext rest;
  16.361                                      in list_comb (Syntax.const (suffix sfx ext),args@[more'])
  16.362                                      end
  16.363                               | NONE => raise TERM(msg ^ "no fields defined for "
  16.364 @@ -548,12 +538,12 @@
  16.365            | NONE => raise TERM (msg ^ name ^" is no proper field",[t]))
  16.366        | mk_ext [] = more
  16.367  
  16.368 -  in mk_ext fieldargs end;   
  16.369 +  in mk_ext fieldargs end;
  16.370  
  16.371  fun gen_ext_type_tr sep mark sfx more sg t =
  16.372 -  let 
  16.373 +  let
  16.374      val msg = "error in record-type input: ";
  16.375 -    val fieldargs = dest_ext_fields sep mark t; 
  16.376 +    val fieldargs = dest_ext_fields sep mark t;
  16.377      fun splitargs (field::fields) ((name,arg)::fargs) =
  16.378            if can (unsuffix name) field
  16.379            then let val (args,rest) = splitargs fields fargs
  16.380 @@ -563,77 +553,77 @@
  16.381        | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t])
  16.382        | splitargs _ _ = ([],[]);
  16.383  
  16.384 -    fun get_sort xs n = (case assoc (xs,n) of 
  16.385 -                                SOME s => s 
  16.386 +    fun get_sort xs n = (case assoc (xs,n) of
  16.387 +                                SOME s => s
  16.388                                | NONE => Sign.defaultS sg);
  16.389 -    
  16.390 - 
  16.391 +
  16.392 +
  16.393      fun to_type t = Sign.certify_typ sg
  16.394 -                       (Sign.intern_typ sg 
  16.395 +                       (Sign.intern_typ sg
  16.396                           (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t));
  16.397  
  16.398      fun mk_ext (fargs as (name,arg)::_) =
  16.399           (case get_fieldext sg (Sign.intern_const sg name) of
  16.400 -            SOME (ext,alphas) => 
  16.401 +            SOME (ext,alphas) =>
  16.402                (case get_extfields sg ext of
  16.403 -                 SOME flds 
  16.404 +                 SOME flds
  16.405                    => (let
  16.406                         val flds' = but_last flds;
  16.407 -                       val types = map snd flds'; 
  16.408 +                       val types = map snd flds';
  16.409                         val (args,rest) = splitargs (map fst flds') fargs;
  16.410                         val vartypes = map Type.varifyT types;
  16.411                         val argtypes = map to_type args;
  16.412                         val (subst,_) = fold (Sign.typ_unify sg) (vartypes ~~ argtypes)
  16.413                                              (Vartab.empty,0);
  16.414 -                       val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o 
  16.415 -                                          Envir.norm_type subst o Type.varifyT) 
  16.416 +                       val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o
  16.417 +                                          Envir.norm_type subst o Type.varifyT)
  16.418                                           (but_last alphas);
  16.419 - 
  16.420 -                       val more' = mk_ext rest;   
  16.421 -                     in list_comb (Syntax.const (suffix sfx ext),alphas'@[more']) 
  16.422 -                     end handle TUNIFY => raise 
  16.423 +
  16.424 +                       val more' = mk_ext rest;
  16.425 +                     in list_comb (Syntax.const (suffix sfx ext),alphas'@[more'])
  16.426 +                     end handle TUNIFY => raise
  16.427                             TERM (msg ^ "type is no proper record (extension)", [t]))
  16.428                 | NONE => raise TERM (msg ^ "no fields defined for " ^ ext,[t]))
  16.429            | NONE => raise TERM (msg ^ name ^" is no proper field",[t]))
  16.430        | mk_ext [] = more
  16.431  
  16.432 -  in mk_ext fieldargs end;   
  16.433 +  in mk_ext fieldargs end;
  16.434  
  16.435 -fun gen_adv_record_tr sep mark sfx unit sg [t] = 
  16.436 +fun gen_adv_record_tr sep mark sfx unit sg [t] =
  16.437        gen_ext_fields_tr sep mark sfx unit sg t
  16.438    | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
  16.439  
  16.440 -fun gen_adv_record_scheme_tr sep mark sfx sg [t, more] = 
  16.441 -      gen_ext_fields_tr sep mark sfx more sg t 
  16.442 +fun gen_adv_record_scheme_tr sep mark sfx sg [t, more] =
  16.443 +      gen_ext_fields_tr sep mark sfx more sg t
  16.444    | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
  16.445  
  16.446 -fun gen_adv_record_type_tr sep mark sfx unit sg [t] = 
  16.447 +fun gen_adv_record_type_tr sep mark sfx unit sg [t] =
  16.448        gen_ext_type_tr sep mark sfx unit sg t
  16.449    | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
  16.450  
  16.451 -fun gen_adv_record_type_scheme_tr sep mark sfx sg [t, more] = 
  16.452 -      gen_ext_type_tr sep mark sfx more sg t 
  16.453 +fun gen_adv_record_type_scheme_tr sep mark sfx sg [t, more] =
  16.454 +      gen_ext_type_tr sep mark sfx more sg t
  16.455    | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
  16.456  
  16.457  val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit;
  16.458  val adv_record_scheme_tr = gen_adv_record_scheme_tr "_fields" "_field" extN;
  16.459  
  16.460 -val adv_record_type_tr = 
  16.461 -      gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN 
  16.462 +val adv_record_type_tr =
  16.463 +      gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN
  16.464          (Syntax.term_of_typ false (HOLogic.unitT));
  16.465 -val adv_record_type_scheme_tr = 
  16.466 +val adv_record_type_scheme_tr =
  16.467        gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
  16.468  
  16.469  
  16.470  val parse_translation =
  16.471   [("_record_update", record_update_tr),
  16.472 -  ("_update_name", update_name_tr)]; 
  16.473 +  ("_update_name", update_name_tr)];
  16.474  
  16.475 -val adv_parse_translation = 
  16.476 +val adv_parse_translation =
  16.477   [("_record",adv_record_tr),
  16.478    ("_record_scheme",adv_record_scheme_tr),
  16.479    ("_record_type",adv_record_type_tr),
  16.480 -  ("_record_type_scheme",adv_record_type_scheme_tr)]; 
  16.481 +  ("_record_type_scheme",adv_record_type_scheme_tr)];
  16.482  
  16.483  (* print translations *)
  16.484  
  16.485 @@ -658,18 +648,18 @@
  16.486    in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
  16.487  
  16.488  fun record_tr' sep mark record record_scheme unit sg t =
  16.489 -  let 
  16.490 +  let
  16.491      fun field_lst t =
  16.492        (case strip_comb t of
  16.493 -        (Const (ext,_),args) 
  16.494 +        (Const (ext,_),args)
  16.495           => (case try (unsuffix extN) (Sign.intern_const sg ext) of
  16.496 -               SOME ext' 
  16.497 +               SOME ext'
  16.498                 => (case get_extfields sg ext' of
  16.499 -                     SOME flds 
  16.500 +                     SOME flds
  16.501                       => (let
  16.502                            val (f::fs) = but_last (map fst flds);
  16.503 -                          val flds' = Sign.extern_const sg f :: map NameSpace.base fs; 
  16.504 -                          val (args',more) = split_last args; 
  16.505 +                          val flds' = Sign.extern_const sg f :: map NameSpace.base fs;
  16.506 +                          val (args',more) = split_last args;
  16.507                           in (flds'~~args')@field_lst more end
  16.508                           handle UnequalLengths => [("",t)])
  16.509                     | NONE => [("",t)])
  16.510 @@ -681,15 +671,15 @@
  16.511      val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds';
  16.512  
  16.513    in if null flds then raise Match
  16.514 -     else if unit more  
  16.515 -          then Syntax.const record$flds'' 
  16.516 +     else if unit more
  16.517 +          then Syntax.const record$flds''
  16.518            else Syntax.const record_scheme$flds''$more
  16.519    end
  16.520  
  16.521 -fun gen_record_tr' name = 
  16.522 +fun gen_record_tr' name =
  16.523    let val name_sfx = suffix extN name;
  16.524        val unit = (fn Const ("Unity",_) => true | _ => false);
  16.525 -      fun tr' sg ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit sg 
  16.526 +      fun tr' sg ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit sg
  16.527                         (list_comb (Syntax.const name_sfx,ts))
  16.528    in (name_sfx,tr')
  16.529    end
  16.530 @@ -704,46 +694,46 @@
  16.531        (* tm is term representation of a (nested) field type. We first reconstruct the      *)
  16.532        (* type from tm so that we can continue on the type level rather then the term level.*)
  16.533  
  16.534 -      fun get_sort xs n = (case assoc (xs,n) of 
  16.535 -                             SOME s => s 
  16.536 +      fun get_sort xs n = (case assoc (xs,n) of
  16.537 +                             SOME s => s
  16.538                             | NONE => Sign.defaultS sg);
  16.539  
  16.540        (* WORKAROUND:
  16.541 -       * If a record type occurs in an error message of type inference there  
  16.542 +       * If a record type occurs in an error message of type inference there
  16.543         * may be some internal frees donoted by ??:
  16.544 -       * (Const "_tfree",_)$Free ("??'a",_). 
  16.545 -         
  16.546 -       * This will unfortunately be translated to Type ("??'a",[]) instead of 
  16.547 -       * TFree ("??'a",_) by typ_of_term, which will confuse unify below. 
  16.548 +       * (Const "_tfree",_)$Free ("??'a",_).
  16.549 +
  16.550 +       * This will unfortunately be translated to Type ("??'a",[]) instead of
  16.551 +       * TFree ("??'a",_) by typ_of_term, which will confuse unify below.
  16.552         * fixT works around.
  16.553         *)
  16.554 -      fun fixT (T as Type (x,[])) = 
  16.555 +      fun fixT (T as Type (x,[])) =
  16.556              if String.isPrefix "??'" x then TFree (x,Sign.defaultS sg) else T
  16.557          | fixT (Type (x,xs)) = Type (x,map fixT xs)
  16.558          | fixT T = T;
  16.559 -      
  16.560 -      val T = fixT (Sign.intern_typ sg 
  16.561 -                      (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm)); 
  16.562 +
  16.563 +      val T = fixT (Sign.intern_typ sg
  16.564 +                      (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm));
  16.565  
  16.566 -      fun mk_type_abbr subst name alphas = 
  16.567 +      fun mk_type_abbr subst name alphas =
  16.568            let val abbrT = Type (name, map (fn a => TVar ((a, 0), Sign.defaultS sg)) alphas);
  16.569 -          in Syntax.term_of_typ (! Syntax.show_sorts) 
  16.570 -               (Sign.extern_typ sg (Envir.norm_type subst abbrT)) end;    
  16.571 +          in Syntax.term_of_typ (! Syntax.show_sorts)
  16.572 +               (Sign.extern_typ sg (Envir.norm_type subst abbrT)) end;
  16.573  
  16.574        fun unify rT T = fst (Sign.typ_unify sg (Type.varifyT rT,T) (Vartab.empty,0));
  16.575  
  16.576     in if !print_record_type_abbr
  16.577        then (case last_extT T of
  16.578 -             SOME (name,_) 
  16.579 -              => if name = lastExt 
  16.580 +             SOME (name,_)
  16.581 +              => if name = lastExt
  16.582                   then
  16.583 -		  (let
  16.584 -                     val subst = unify schemeT T 
  16.585 -                   in 
  16.586 +                  (let
  16.587 +                     val subst = unify schemeT T
  16.588 +                   in
  16.589                      if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg)))
  16.590                      then mk_type_abbr subst abbr alphas
  16.591                      else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
  16.592 -		   end handle TUNIFY => default_tr' sg tm)
  16.593 +                   end handle TUNIFY => default_tr' sg tm)
  16.594                   else raise Match (* give print translation of specialised record a chance *)
  16.595              | _ => raise Match)
  16.596         else default_tr' sg tm
  16.597 @@ -751,39 +741,39 @@
  16.598  
  16.599  fun record_type_tr' sep mark record record_scheme sg t =
  16.600    let
  16.601 -    fun get_sort xs n = (case assoc (xs,n) of 
  16.602 -                             SOME s => s 
  16.603 +    fun get_sort xs n = (case assoc (xs,n) of
  16.604 +                             SOME s => s
  16.605                             | NONE => Sign.defaultS sg);
  16.606  
  16.607      val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)
  16.608  
  16.609      fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ sg T);
  16.610 - 
  16.611 +
  16.612      fun field_lst T =
  16.613        (case T of
  16.614 -        Type (ext,args) 
  16.615 +        Type (ext,args)
  16.616           => (case try (unsuffix ext_typeN) ext of
  16.617 -               SOME ext' 
  16.618 +               SOME ext'
  16.619                 => (case get_extfields sg ext' of
  16.620 -                     SOME flds 
  16.621 +                     SOME flds
  16.622                       => (case get_fieldext sg (fst (hd flds)) of
  16.623 -                           SOME (_,alphas) 
  16.624 +                           SOME (_,alphas)
  16.625                             => (let
  16.626                                  val (f::fs) = but_last flds;
  16.627                                  val flds' = apfst (Sign.extern_const sg) f
  16.628 -                                            ::map (apfst NameSpace.base) fs; 
  16.629 -                                val (args',more) = split_last args; 
  16.630 -                                val alphavars = map Type.varifyT (but_last alphas); 
  16.631 +                                            ::map (apfst NameSpace.base) fs;
  16.632 +                                val (args',more) = split_last args;
  16.633 +                                val alphavars = map Type.varifyT (but_last alphas);
  16.634                                  val (subst,_)= fold (Sign.typ_unify sg) (alphavars~~args')
  16.635                                                      (Vartab.empty,0);
  16.636                                  val flds'' =map (apsnd (Envir.norm_type subst o Type.varifyT))
  16.637                                                  flds';
  16.638                                in flds''@field_lst more end
  16.639 -                              handle TUNIFY         => [("",T)] 
  16.640 +                              handle TUNIFY         => [("",T)]
  16.641                                     | UnequalLengths => [("",T)])
  16.642                           | NONE => [("",T)])
  16.643                     | NONE => [("",T)])
  16.644 -             | NONE => [("",T)]) 
  16.645 +             | NONE => [("",T)])
  16.646          | _ => [("",T)])
  16.647  
  16.648      val (flds,(_,moreT)) = split_last (field_lst T);
  16.649 @@ -791,25 +781,25 @@
  16.650      val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds';
  16.651  
  16.652    in if not (!print_record_type_as_fields) orelse null flds then raise Match
  16.653 -     else if moreT = HOLogic.unitT 
  16.654 -          then Syntax.const record$flds'' 
  16.655 +     else if moreT = HOLogic.unitT
  16.656 +          then Syntax.const record$flds''
  16.657            else Syntax.const record_scheme$flds''$term_of_type moreT
  16.658    end
  16.659 -    
  16.660 +
  16.661  
  16.662 -fun gen_record_type_tr' name = 
  16.663 +fun gen_record_type_tr' name =
  16.664    let val name_sfx = suffix ext_typeN name;
  16.665 -      fun tr' sg ts = record_type_tr' "_field_types" "_field_type" 
  16.666 -                       "_record_type" "_record_type_scheme" sg 
  16.667 +      fun tr' sg ts = record_type_tr' "_field_types" "_field_type"
  16.668 +                       "_record_type" "_record_type_scheme" sg
  16.669                         (list_comb (Syntax.const name_sfx,ts))
  16.670    in (name_sfx,tr')
  16.671    end
  16.672  
  16.673 -     
  16.674 +
  16.675  fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name =
  16.676    let val name_sfx = suffix ext_typeN name;
  16.677 -      val default_tr' = record_type_tr' "_field_types" "_field_type" 
  16.678 -                               "_record_type" "_record_type_scheme" 
  16.679 +      val default_tr' = record_type_tr' "_field_types" "_field_type"
  16.680 +                               "_record_type" "_record_type_scheme"
  16.681        fun tr' sg ts = record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg
  16.682                           (list_comb (Syntax.const name_sfx,ts))
  16.683    in (name_sfx, tr') end;
  16.684 @@ -824,27 +814,27 @@
  16.685    then Tactic.prove sg [] [] (Logic.list_implies (map Logic.varify asms,Logic.varify prop))
  16.686          (K (SkipProof.cheat_tac HOL.thy))
  16.687          (* standard can take quite a while for large records, thats why
  16.688 -         * we varify the proposition manually here.*) 
  16.689 +         * we varify the proposition manually here.*)
  16.690    else let val prf = Tactic.prove sg [] asms prop tac;
  16.691 -       in if stndrd then standard prf else prf end; 
  16.692 +       in if stndrd then standard prf else prf end;
  16.693  
  16.694 -fun quick_and_dirty_prf noopt opt () = 
  16.695 -      if !record_quick_and_dirty_sensitive andalso !quick_and_dirty 
  16.696 +fun quick_and_dirty_prf noopt opt () =
  16.697 +      if !record_quick_and_dirty_sensitive andalso !quick_and_dirty
  16.698        then noopt ()
  16.699        else opt ();
  16.700  
  16.701  
  16.702  fun prove_split_simp sg ss T prop =
  16.703 -  let 
  16.704 +  let
  16.705      val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg;
  16.706 -    val extsplits = 
  16.707 -            Library.foldl (fn (thms,(n,_)) => (list (Symtab.lookup (extsplit,n)))@thms) 
  16.708 +    val extsplits =
  16.709 +            Library.foldl (fn (thms,(n,_)) => list (Symtab.curried_lookup extsplit n) @ thms)
  16.710                      ([],dest_recTs T);
  16.711      val thms = (case get_splits sg (rec_id (~1) T) of
  16.712 -                   SOME (all_thm,_,_,_) => 
  16.713 +                   SOME (all_thm,_,_,_) =>
  16.714                       all_thm::(case extsplits of [thm] => [] | _ => extsplits)
  16.715                                (* [thm] is the same as all_thm *)
  16.716 -                 | NONE => extsplits)                                
  16.717 +                 | NONE => extsplits)
  16.718    in
  16.719      quick_and_dirty_prove true sg [] prop
  16.720        (fn _ => simp_tac (Simplifier.inherit_bounds ss simpset addsimps thms) 1)
  16.721 @@ -854,7 +844,7 @@
  16.722  local
  16.723  fun eq (s1:string) (s2:string) = (s1 = s2);
  16.724  fun has_field extfields f T =
  16.725 -     exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_multi (extfields,eN))) 
  16.726 +     exists (fn (eN,_) => exists (eq f o fst) (Symtab.curried_lookup_multi extfields eN))
  16.727         (dest_recTs T);
  16.728  in
  16.729  (* record_simproc *)
  16.730 @@ -867,7 +857,7 @@
  16.731   * - If S is a more-selector we have to make sure that the update on component
  16.732   *   X does not affect the selected subrecord.
  16.733   * - If X is a more-selector we have to make sure that S is not in the updated
  16.734 - *   subrecord. 
  16.735 + *   subrecord.
  16.736   *)
  16.737  val record_simproc =
  16.738    Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
  16.739 @@ -878,42 +868,42 @@
  16.740            (case get_updates sg u of SOME u_name =>
  16.741              let
  16.742                val {sel_upd={updates,...},extfields,...} = RecordsData.get sg;
  16.743 -              
  16.744 +
  16.745                fun mk_eq_terms ((upd as Const (u,Type(_,[kT,_]))) $ k $ r) =
  16.746 -		  (case (Symtab.lookup (updates,u)) of
  16.747 +                  (case Symtab.curried_lookup updates u of
  16.748                       NONE => NONE
  16.749 -                   | SOME u_name 
  16.750 +                   | SOME u_name
  16.751                       => if u_name = s
  16.752 -                        then let 
  16.753 +                        then let
  16.754                                 val rv = ("r",rT)
  16.755                                 val rb = Bound 0
  16.756                                 val kv = ("k",kT)
  16.757 -                               val kb = Bound 1 
  16.758 +                               val kb = Bound 1
  16.759                               in SOME (upd$kb$rb,kb,[kv,rv],true) end
  16.760                          else if has_field extfields u_name rangeS
  16.761                               orelse has_field extfields s kT
  16.762                               then NONE
  16.763 -			     else (case mk_eq_terms r of 
  16.764 -                                     SOME (trm,trm',vars,update_s) 
  16.765 -                                     => let   
  16.766 -					  val kv = ("k",kT)
  16.767 +                             else (case mk_eq_terms r of
  16.768 +                                     SOME (trm,trm',vars,update_s)
  16.769 +                                     => let
  16.770 +                                          val kv = ("k",kT)
  16.771                                            val kb = Bound (length vars)
  16.772 -		                        in SOME (upd$kb$trm,trm',kv::vars,update_s) end
  16.773 +                                        in SOME (upd$kb$trm,trm',kv::vars,update_s) end
  16.774                                     | NONE
  16.775 -                                     => let 
  16.776 -					  val rv = ("r",rT)
  16.777 +                                     => let
  16.778 +                                          val rv = ("r",rT)
  16.779                                            val rb = Bound 0
  16.780                                            val kv = ("k",kT)
  16.781 -                                          val kb = Bound 1 
  16.782 +                                          val kb = Bound 1
  16.783                                          in SOME (upd$kb$rb,rb,[kv,rv],false) end))
  16.784 -                | mk_eq_terms r = NONE     
  16.785 +                | mk_eq_terms r = NONE
  16.786              in
  16.787 -	      (case mk_eq_terms (upd$k$r) of
  16.788 -                 SOME (trm,trm',vars,update_s) 
  16.789 -                 => if update_s 
  16.790 -		    then SOME (prove_split_simp sg ss domS 
  16.791 +              (case mk_eq_terms (upd$k$r) of
  16.792 +                 SOME (trm,trm',vars,update_s)
  16.793 +                 => if update_s
  16.794 +                    then SOME (prove_split_simp sg ss domS
  16.795                                   (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
  16.796 -                    else SOME (prove_split_simp sg ss domS 
  16.797 +                    else SOME (prove_split_simp sg ss domS
  16.798                                   (list_all(vars,(equals rangeS$(sel$trm)$(sel$trm')))))
  16.799                 | NONE => NONE)
  16.800              end
  16.801 @@ -921,91 +911,91 @@
  16.802          | NONE => NONE)
  16.803        | _ => NONE));
  16.804  
  16.805 -(* record_upd_simproc *) 
  16.806 +(* record_upd_simproc *)
  16.807  (* simplify multiple updates:
  16.808   *  (1)  "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)"
  16.809   *  (2)  "r(|M:= M r|) = r"
  16.810   * For (2) special care of "more" updates has to be taken:
  16.811   *    r(|more := m; A := A r|)
  16.812   * If A is contained in the fields of m we cannot remove the update A := A r!
  16.813 - * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|) 
  16.814 + * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|)
  16.815  *)
  16.816  val record_upd_simproc =
  16.817    Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u k r)"]
  16.818      (fn sg => fn ss => fn t =>
  16.819        (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) =>
  16.820 - 	 let datatype ('a,'b) calc = Init of 'b | Inter of 'a  
  16.821 +         let datatype ('a,'b) calc = Init of 'b | Inter of 'a
  16.822               val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg;
  16.823 -             
  16.824 -	     (*fun mk_abs_var x t = (x, fastype_of t);*)
  16.825 +
  16.826 +             (*fun mk_abs_var x t = (x, fastype_of t);*)
  16.827               fun sel_name u = NameSpace.base (unsuffix updateN u);
  16.828  
  16.829               fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
  16.830                    if has_field extfields s mT then upd else seed s r
  16.831                 | seed _ r = r;
  16.832  
  16.833 -             fun grow u uT k kT vars (sprout,skeleton) = 
  16.834 -		   if sel_name u = moreN
  16.835 +             fun grow u uT k kT vars (sprout,skeleton) =
  16.836 +                   if sel_name u = moreN
  16.837                     then let val kv = ("k", kT);
  16.838                              val kb = Bound (length vars);
  16.839                          in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
  16.840                     else ((sprout,skeleton),vars);
  16.841  
  16.842               fun is_upd_same (sprout,skeleton) u ((sel as Const (s,_))$r) =
  16.843 -                   if (unsuffix updateN u) = s andalso (seed s sprout) = r 
  16.844 +                   if (unsuffix updateN u) = s andalso (seed s sprout) = r
  16.845                     then SOME (sel,seed s skeleton)
  16.846                     else NONE
  16.847                 | is_upd_same _ _ _ = NONE
  16.848 - 
  16.849 +
  16.850               fun init_seed r = ((r,Bound 0), [("r", rT)]);
  16.851 -                       
  16.852 +
  16.853               (* mk_updterm returns either
  16.854                *  - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made,
  16.855 -              *     where vars are the bound variables in the skeleton 
  16.856 -              *  - Inter (orig-term-skeleton,simplified-term-skeleton, 
  16.857 +              *     where vars are the bound variables in the skeleton
  16.858 +              *  - Inter (orig-term-skeleton,simplified-term-skeleton,
  16.859                *           vars, (term-sprout, skeleton-sprout))
  16.860                *     where "All vars. orig-term-skeleton = simplified-term-skeleton" is
  16.861                *     the desired simplification rule,
  16.862                *     the sprouts accumulate the "more-updates" on the way from the seed
  16.863 -              *     to the outermost update. It is only relevant to calculate the 
  16.864 -              *     possible simplification for (2) 
  16.865 +              *     to the outermost update. It is only relevant to calculate the
  16.866 +              *     possible simplification for (2)
  16.867                * The algorithm first walks down the updates to the seed-record while
  16.868                * memorising the updates in the already-table. While walking up the
  16.869                * updates again, the optimised term is constructed.
  16.870                *)
  16.871 -             fun mk_updterm upds already 
  16.872 +             fun mk_updterm upds already
  16.873                   (t as ((upd as Const (u,uT as (Type (_,[kT,_])))) $ k $ r)) =
  16.874 -		 if isSome (Symtab.lookup (upds,u))
  16.875 -		 then let 
  16.876 -			 fun rest already = mk_updterm upds already
  16.877 -		      in if u mem_string already 
  16.878 -			 then (case (rest already r) of
  16.879 -				 Init ((sprout,skel),vars) => 
  16.880 +                 if Symtab.defined upds u
  16.881 +                 then let
  16.882 +                         fun rest already = mk_updterm upds already
  16.883 +                      in if u mem_string already
  16.884 +                         then (case (rest already r) of
  16.885 +                                 Init ((sprout,skel),vars) =>
  16.886                                   let
  16.887 -	                           val kv = (sel_name u, kT);
  16.888 +                                   val kv = (sel_name u, kT);
  16.889                                     val kb = Bound (length vars);
  16.890                                     val (sprout',vars')= grow u uT k kT (kv::vars) (sprout,skel);
  16.891                                   in Inter (upd$kb$skel,skel,vars',sprout') end
  16.892 -                               | Inter (trm,trm',vars,sprout) => 
  16.893 -                                 let 
  16.894 -		                   val kv = (sel_name u, kT);
  16.895 +                               | Inter (trm,trm',vars,sprout) =>
  16.896 +                                 let
  16.897 +                                   val kv = (sel_name u, kT);
  16.898                                     val kb = Bound (length vars);
  16.899                                     val (sprout',vars') = grow u uT k kT (kv::vars) sprout;
  16.900 -                                 in Inter(upd$kb$trm,trm',kv::vars',sprout') end) 
  16.901 -	                 else 
  16.902 -                          (case rest (u::already) r of 
  16.903 -			     Init ((sprout,skel),vars) => 
  16.904 +                                 in Inter(upd$kb$trm,trm',kv::vars',sprout') end)
  16.905 +                         else
  16.906 +                          (case rest (u::already) r of
  16.907 +                             Init ((sprout,skel),vars) =>
  16.908                                (case is_upd_same (sprout,skel) u k of
  16.909 -                                 SOME (sel,skel') => 
  16.910 +                                 SOME (sel,skel') =>
  16.911                                   let
  16.912 -		                   val (sprout',vars') = grow u uT k kT vars (sprout,skel); 
  16.913 +                                   val (sprout',vars') = grow u uT k kT vars (sprout,skel);
  16.914                                    in Inter(upd$(sel$skel')$skel,skel,vars',sprout') end
  16.915 -                               | NONE =>  
  16.916 +                               | NONE =>
  16.917                                   let
  16.918 -	                           val kv = (sel_name u, kT);
  16.919 +                                   val kv = (sel_name u, kT);
  16.920                                     val kb = Bound (length vars);
  16.921                                   in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end)
  16.922 -		           | Inter (trm,trm',vars,sprout) => 
  16.923 +                           | Inter (trm,trm',vars,sprout) =>
  16.924                                 (case is_upd_same sprout u k of
  16.925                                    SOME (sel,skel) =>
  16.926                                    let
  16.927 @@ -1013,20 +1003,20 @@
  16.928                                    in Inter(upd$(sel$skel)$trm,trm',vars',sprout') end
  16.929                                  | NONE =>
  16.930                                    let
  16.931 -				    val kv = (sel_name u, kT)
  16.932 +                                    val kv = (sel_name u, kT)
  16.933                                      val kb = Bound (length vars)
  16.934                                      val (sprout',vars') = grow u uT k kT (kv::vars) sprout
  16.935                                    in Inter (upd$kb$trm,upd$kb$trm',vars',sprout') end))
  16.936 -		      end
  16.937 -		 else Init (init_seed t)
  16.938 -	       | mk_updterm _ _ t = Init (init_seed t);
  16.939 +                      end
  16.940 +                 else Init (init_seed t)
  16.941 +               | mk_updterm _ _ t = Init (init_seed t);
  16.942  
  16.943 -	 in (case mk_updterm updates [] t of
  16.944 -	       Inter (trm,trm',vars,_)
  16.945 -                => SOME (prove_split_simp sg ss rT  
  16.946 +         in (case mk_updterm updates [] t of
  16.947 +               Inter (trm,trm',vars,_)
  16.948 +                => SOME (prove_split_simp sg ss rT
  16.949                            (list_all(vars,(equals rT$trm$trm'))))
  16.950               | _ => NONE)
  16.951 -	 end
  16.952 +         end
  16.953         | _ => NONE));
  16.954  end
  16.955  
  16.956 @@ -1040,8 +1030,8 @@
  16.957   * e.g. r(|lots of updates|) = x
  16.958   *
  16.959   *               record_eq_simproc       record_split_simp_tac
  16.960 - * Complexity: #components * #updates     #updates   
  16.961 - *           
  16.962 + * Complexity: #components * #updates     #updates
  16.963 + *
  16.964   *)
  16.965  val record_eq_simproc =
  16.966    Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"]
  16.967 @@ -1055,7 +1045,7 @@
  16.968         | _ => NONE));
  16.969  
  16.970  (* record_split_simproc *)
  16.971 -(* splits quantified occurrences of records, for which P holds. P can peek on the 
  16.972 +(* splits quantified occurrences of records, for which P holds. P can peek on the
  16.973   * subterm starting at the quantified occurrence of the record (including the quantifier)
  16.974   * P t = 0: do not split
  16.975   * P t = ~1: completely split
  16.976 @@ -1069,11 +1059,11 @@
  16.977           then (case rec_id (~1) T of
  16.978                   "" => NONE
  16.979                 | name
  16.980 -                  => let val split = P t 
  16.981 -                     in if split <> 0 then 
  16.982 +                  => let val split = P t
  16.983 +                     in if split <> 0 then
  16.984                          (case get_splits sg (rec_id split T) of
  16.985                                NONE => NONE
  16.986 -                            | SOME (all_thm, All_thm, Ex_thm,_) 
  16.987 +                            | SOME (all_thm, All_thm, Ex_thm,_)
  16.988                                 => SOME (case quantifier of
  16.989                                            "all" => all_thm
  16.990                                          | "All" => All_thm RS HOL.eq_reflection
  16.991 @@ -1087,7 +1077,7 @@
  16.992  val record_ex_sel_eq_simproc =
  16.993    Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"]
  16.994      (fn sg => fn ss => fn t =>
  16.995 -       let 
  16.996 +       let
  16.997           fun prove prop =
  16.998             quick_and_dirty_prove true sg [] prop
  16.999               (fn _ => simp_tac (Simplifier.inherit_bounds ss (get_simpset sg)
 16.1000 @@ -1095,22 +1085,22 @@
 16.1001  
 16.1002           fun mkeq (lr,Teq,(sel,Tsel),x) i =
 16.1003                (case get_selectors sg sel of SOME () =>
 16.1004 -                 let val x' = if not (loose_bvar1 (x,0)) 
 16.1005 -                              then Free ("x" ^ string_of_int i, range_type Tsel) 
 16.1006 +                 let val x' = if not (loose_bvar1 (x,0))
 16.1007 +                              then Free ("x" ^ string_of_int i, range_type Tsel)
 16.1008                                else raise TERM ("",[x]);
 16.1009                       val sel' = Const (sel,Tsel)$Bound 0;
 16.1010                       val (l,r) = if lr then (sel',x') else (x',sel');
 16.1011                    in Const ("op =",Teq)$l$r end
 16.1012                 | NONE => raise TERM ("",[Const (sel,Tsel)]));
 16.1013  
 16.1014 -         fun dest_sel_eq (Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X) = 
 16.1015 +         fun dest_sel_eq (Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X) =
 16.1016                             (true,Teq,(sel,Tsel),X)
 16.1017             | dest_sel_eq (Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0)) =
 16.1018                             (false,Teq,(sel,Tsel),X)
 16.1019             | dest_sel_eq _ = raise TERM ("",[]);
 16.1020  
 16.1021 -       in         
 16.1022 -         (case t of 
 16.1023 +       in
 16.1024 +         (case t of
 16.1025             (Const ("Ex",Tex)$Abs(s,T,t)) =>
 16.1026               (let val eq = mkeq (dest_sel_eq t) 0;
 16.1027                   val prop = list_all ([("r",T)],
 16.1028 @@ -1118,54 +1108,54 @@
 16.1029                                                 HOLogic.true_const));
 16.1030               in SOME (prove prop) end
 16.1031               handle TERM _ => NONE)
 16.1032 -          | _ => NONE)                      
 16.1033 +          | _ => NONE)
 16.1034           end)
 16.1035  
 16.1036  
 16.1037 -    
 16.1038 +
 16.1039  
 16.1040  local
 16.1041  val inductive_atomize = thms "induct_atomize";
 16.1042  val inductive_rulify1 = thms "induct_rulify1";
 16.1043  in
 16.1044  (* record_split_simp_tac *)
 16.1045 -(* splits (and simplifies) all records in the goal for which P holds. 
 16.1046 +(* splits (and simplifies) all records in the goal for which P holds.
 16.1047   * For quantified occurrences of a record
 16.1048   * P can peek on the whole subterm (including the quantifier); for free variables P
 16.1049   * can only peek on the variable itself.
 16.1050   * P t = 0: do not split
 16.1051   * P t = ~1: completely split
 16.1052 - * P t > 0: split up to given bound of record extensions 
 16.1053 + * P t > 0: split up to given bound of record extensions
 16.1054   *)
 16.1055  fun record_split_simp_tac thms P i st =
 16.1056    let
 16.1057      val sg = Thm.sign_of_thm st;
 16.1058 -    val {sel_upd={simpset,...},...} 
 16.1059 +    val {sel_upd={simpset,...},...}
 16.1060              = RecordsData.get sg;
 16.1061  
 16.1062      val has_rec = exists_Const
 16.1063        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
 16.1064 -          (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T 
 16.1065 +          (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T
 16.1066          | _ => false);
 16.1067  
 16.1068      val goal = List.nth (Thm.prems_of st, i - 1);
 16.1069      val frees = List.filter (is_recT o type_of) (term_frees goal);
 16.1070  
 16.1071 -    fun mk_split_free_tac free induct_thm i = 
 16.1072 -	let val cfree = cterm_of sg free;
 16.1073 +    fun mk_split_free_tac free induct_thm i =
 16.1074 +        let val cfree = cterm_of sg free;
 16.1075              val (_$(_$r)) = concl_of induct_thm;
 16.1076              val crec = cterm_of sg r;
 16.1077              val thm  = cterm_instantiate [(crec,cfree)] induct_thm;
 16.1078          in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
 16.1079                    rtac thm i,
 16.1080                    simp_tac (HOL_basic_ss addsimps inductive_rulify1) i]
 16.1081 -	end;
 16.1082 +        end;
 16.1083  
 16.1084 -    fun split_free_tac P i (free as Free (n,T)) = 
 16.1085 -	(case rec_id (~1) T of
 16.1086 +    fun split_free_tac P i (free as Free (n,T)) =
 16.1087 +        (case rec_id (~1) T of
 16.1088             "" => NONE
 16.1089 -         | name => let val split = P free 
 16.1090 -                   in if split <> 0 then 
 16.1091 +         | name => let val split = P free
 16.1092 +                   in if split <> 0 then
 16.1093                        (case get_splits sg (rec_id split T) of
 16.1094                               NONE => NONE
 16.1095                             | SOME (_,_,_,induct_thm)
 16.1096 @@ -1175,10 +1165,10 @@
 16.1097       | split_free_tac _ _ _ = NONE;
 16.1098  
 16.1099      val split_frees_tacs = List.mapPartial (split_free_tac P i) frees;
 16.1100 -   
 16.1101 +
 16.1102      val simprocs = if has_rec goal then [record_split_simproc P] else [];
 16.1103 -   
 16.1104 -  in st |> ((EVERY split_frees_tacs) 
 16.1105 +
 16.1106 +  in st |> ((EVERY split_frees_tacs)
 16.1107             THEN (Simplifier.full_simp_tac (simpset addsimps thms addsimprocs simprocs) i))
 16.1108    end handle Empty => Seq.empty;
 16.1109  end;
 16.1110 @@ -1192,19 +1182,19 @@
 16.1111  
 16.1112      val has_rec = exists_Const
 16.1113        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
 16.1114 -          (s = "all" orelse s = "All") andalso is_recT T 
 16.1115 +          (s = "all" orelse s = "All") andalso is_recT T
 16.1116          | _ => false);
 16.1117 - 
 16.1118 -    val goal = List.nth (Thm.prems_of st, i - 1);   
 16.1119 +
 16.1120 +    val goal = List.nth (Thm.prems_of st, i - 1);
 16.1121  
 16.1122      fun is_all t =
 16.1123        (case t of (Const (quantifier, _)$_) =>
 16.1124           if quantifier = "All" orelse quantifier = "all" then ~1 else 0
 16.1125         | _ => 0);
 16.1126 - 
 16.1127 -  in if has_rec goal 
 16.1128 -     then Simplifier.full_simp_tac 
 16.1129 -           (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st 
 16.1130 +
 16.1131 +  in if has_rec goal
 16.1132 +     then Simplifier.full_simp_tac
 16.1133 +           (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st
 16.1134       else Seq.empty
 16.1135    end handle Subscript => Seq.empty;
 16.1136  
 16.1137 @@ -1245,10 +1235,10 @@
 16.1138  
 16.1139  fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
 16.1140  
 16.1141 -(* do case analysis / induction according to rule on last parameter of ith subgoal 
 16.1142 - * (or on s if there are no parameters); 
 16.1143 +(* do case analysis / induction according to rule on last parameter of ith subgoal
 16.1144 + * (or on s if there are no parameters);
 16.1145   * Instatiation of record variable (and predicate) in rule is calculated to
 16.1146 - * avoid problems with higher order unification. 
 16.1147 + * avoid problems with higher order unification.
 16.1148   *)
 16.1149  
 16.1150  fun try_param_tac s rule i st =
 16.1151 @@ -1287,10 +1277,10 @@
 16.1152      val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI'));
 16.1153      val cx = cterm_of sg (fst (strip_comb x));
 16.1154  
 16.1155 -  in Seq.single (Library.foldl (fn (st,v) => 
 16.1156 -        Seq.hd 
 16.1157 -        (compose_tac (false, cterm_instantiate 
 16.1158 -                                [(cx,cterm_of sg (list_abs (params,Bound v)))] exI',1) 
 16.1159 +  in Seq.single (Library.foldl (fn (st,v) =>
 16.1160 +        Seq.hd
 16.1161 +        (compose_tac (false, cterm_instantiate
 16.1162 +                                [(cx,cterm_of sg (list_abs (params,Bound v)))] exI',1)
 16.1163                  i st)) (st,((length params) - 1) downto 0))
 16.1164    end;
 16.1165  
 16.1166 @@ -1298,7 +1288,7 @@
 16.1167    let
 16.1168      val UNIV = HOLogic.mk_UNIV repT;
 16.1169  
 16.1170 -    val (thy',{set_def=SOME def, Abs_induct = abs_induct, 
 16.1171 +    val (thy',{set_def=SOME def, Abs_induct = abs_induct,
 16.1172                 Abs_inject=abs_inject, Abs_inverse = abs_inverse,...}) =
 16.1173          thy |> setmp TypedefPackage.quiet_mode true
 16.1174             (TypedefPackage.add_typedef_i true NONE
 16.1175 @@ -1308,12 +1298,12 @@
 16.1176    in (thy',map rewrite_rule [abs_inject, abs_inverse, abs_induct])
 16.1177    end;
 16.1178  
 16.1179 -fun mixit convs refls = 
 16.1180 +fun mixit convs refls =
 16.1181    let fun f ((res,lhs,rhs),refl) = ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs);
 16.1182    in #1 (Library.foldl f (([],[],convs),refls)) end;
 16.1183  
 16.1184 -fun extension_definition full name fields names alphas zeta moreT more vars thy = 
 16.1185 -  let  
 16.1186 +fun extension_definition full name fields names alphas zeta moreT more vars thy =
 16.1187 +  let
 16.1188      val base = Sign.base_name;
 16.1189      val fieldTs = (map snd fields);
 16.1190      val alphas_zeta = alphas@[zeta];
 16.1191 @@ -1330,20 +1320,20 @@
 16.1192      val idxms = 0 upto len;
 16.1193  
 16.1194      (* prepare declarations and definitions *)
 16.1195 -    
 16.1196 +
 16.1197      (*fields constructor*)
 16.1198      val ext_decl = (mk_extC (name,extT) fields_moreTs);
 16.1199 -    (*     
 16.1200 -    val ext_spec = Const ext_decl :== 
 16.1201 -         (foldr (uncurry lambda) 
 16.1202 -            (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))) (vars@[more])) 
 16.1203 -    *) 
 16.1204 -    val ext_spec = list_comb (Const ext_decl,vars@[more]) :== 
 16.1205 +    (*
 16.1206 +    val ext_spec = Const ext_decl :==
 16.1207 +         (foldr (uncurry lambda)
 16.1208 +            (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))) (vars@[more]))
 16.1209 +    *)
 16.1210 +    val ext_spec = list_comb (Const ext_decl,vars@[more]) :==
 16.1211           (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more])));
 16.1212 - 
 16.1213 -    fun mk_ext args = list_comb (Const ext_decl, args); 
 16.1214  
 16.1215 -    (*destructors*) 
 16.1216 +    fun mk_ext args = list_comb (Const ext_decl, args);
 16.1217 +
 16.1218 +    (*destructors*)
 16.1219      val _ = timing_msg "record extension preparing definitions";
 16.1220      val dest_decls = map (mk_selC extT o (apfst (suffix ext_dest))) bfields_more;
 16.1221  
 16.1222 @@ -1354,31 +1344,31 @@
 16.1223        end;
 16.1224      val dest_specs =
 16.1225        ListPair.map mk_dest_spec (idxms, fields_more);
 16.1226 -   
 16.1227 +
 16.1228      (*updates*)
 16.1229      val upd_decls = map (mk_updC updN extT) bfields_more;
 16.1230      fun mk_upd_spec (c,T) =
 16.1231        let
 16.1232 -        val args = map (fn (n,nT) => if n=c then Free (base c,T) 
 16.1233 -                                     else (mk_sel r (suffix ext_dest n,nT))) 
 16.1234 +        val args = map (fn (n,nT) => if n=c then Free (base c,T)
 16.1235 +                                     else (mk_sel r (suffix ext_dest n,nT)))
 16.1236                         fields_more;
 16.1237        in Const (mk_updC updN extT (c,T))$(Free (base c,T))$r
 16.1238            :== mk_ext args
 16.1239        end;
 16.1240      val upd_specs = map mk_upd_spec fields_more;
 16.1241 -    
 16.1242 +
 16.1243      (* 1st stage: defs_thy *)
 16.1244      fun mk_defs () =
 16.1245 -      thy 
 16.1246 +      thy
 16.1247          |> extension_typedef name repT (alphas@[zeta])
 16.1248 -        |>> Theory.add_consts_i 
 16.1249 +        |>> Theory.add_consts_i
 16.1250                (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
 16.1251          |>>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
 16.1252          |>>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs)
 16.1253      val (defs_thy, (([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs),upd_defs)) =
 16.1254          timeit_msg "record extension type/selector/update defs:" mk_defs;
 16.1255 -        
 16.1256 -    
 16.1257 +
 16.1258 +
 16.1259      (* prepare propositions *)
 16.1260      val _ = timing_msg "record extension preparing propositions";
 16.1261      val vars_more = vars@[more];
 16.1262 @@ -1389,70 +1379,70 @@
 16.1263      val w     = Free (wN, extT);
 16.1264      val P = Free (variant variants "P", extT-->HOLogic.boolT);
 16.1265      val C = Free (variant variants "C", HOLogic.boolT);
 16.1266 -    
 16.1267 +
 16.1268      val inject_prop =
 16.1269        let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
 16.1270 -      in All (map dest_Free (vars_more@vars_more')) 
 16.1271 -          ((HOLogic.eq_const extT $ 
 16.1272 -            mk_ext vars_more$mk_ext vars_more') 
 16.1273 +      in All (map dest_Free (vars_more@vars_more'))
 16.1274 +          ((HOLogic.eq_const extT $
 16.1275 +            mk_ext vars_more$mk_ext vars_more')
 16.1276             ===
 16.1277             foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more')))
 16.1278        end;
 16.1279 -    
 16.1280 +
 16.1281      val induct_prop =
 16.1282        (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
 16.1283  
 16.1284      val cases_prop =
 16.1285 -      (All (map dest_Free vars_more) 
 16.1286 -        (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C)) 
 16.1287 +      (All (map dest_Free vars_more)
 16.1288 +        (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C))
 16.1289        ==> Trueprop C;
 16.1290  
 16.1291 -    (*destructors*) 
 16.1292 +    (*destructors*)
 16.1293      val dest_conv_props =
 16.1294         map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more;
 16.1295  
 16.1296      (*updates*)
 16.1297      fun mk_upd_prop (i,(c,T)) =
 16.1298 -      let val x' = Free (variant variants (base c ^ "'"),T) 
 16.1299 +      let val x' = Free (variant variants (base c ^ "'"),T)
 16.1300            val args' = nth_update x' (i, vars_more)
 16.1301        in mk_upd updN c x' ext === mk_ext args'  end;
 16.1302      val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
 16.1303  
 16.1304      val surjective_prop =
 16.1305 -      let val args = 
 16.1306 +      let val args =
 16.1307             map (fn (c, Free (_,T)) => mk_sel s (suffix ext_dest c,T)) named_vars_more;
 16.1308        in s === mk_ext args end;
 16.1309  
 16.1310      val split_meta_prop =
 16.1311        let val P = Free (variant variants "P", extT-->Term.propT) in
 16.1312 -        Logic.mk_equals 
 16.1313 +        Logic.mk_equals
 16.1314           (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
 16.1315 -      end; 
 16.1316 +      end;
 16.1317  
 16.1318      fun prove stndrd = quick_and_dirty_prove stndrd (Theory.sign_of defs_thy);
 16.1319      val prove_standard = quick_and_dirty_prove true (Theory.sign_of defs_thy);
 16.1320      fun prove_simp stndrd simps =
 16.1321        let val tac = simp_all_tac HOL_ss simps
 16.1322        in fn prop => prove stndrd [] prop (K tac) end;
 16.1323 -    
 16.1324 +
 16.1325      fun inject_prf () = (prove_simp true [ext_def,abs_inject,Pair_eq] inject_prop);
 16.1326      val inject = timeit_msg "record extension inject proof:" inject_prf;
 16.1327  
 16.1328      fun induct_prf () =
 16.1329        let val (assm, concl) = induct_prop
 16.1330        in prove_standard [assm] concl (fn prems =>
 16.1331 -           EVERY [try_param_tac rN abs_induct 1, 
 16.1332 +           EVERY [try_param_tac rN abs_induct 1,
 16.1333                    simp_tac (HOL_ss addsimps [split_paired_all]) 1,
 16.1334                    resolve_tac (map (rewrite_rule [ext_def]) prems) 1])
 16.1335        end;
 16.1336      val induct = timeit_msg "record extension induct proof:" induct_prf;
 16.1337  
 16.1338      fun cases_prf_opt () =
 16.1339 -      let 
 16.1340 +      let
 16.1341          val sg = (sign_of defs_thy);
 16.1342          val (_$(Pvar$_)) = concl_of induct;
 16.1343 -        val ind = cterm_instantiate 
 16.1344 -                    [(cterm_of sg Pvar, cterm_of sg 
 16.1345 +        val ind = cterm_instantiate
 16.1346 +                    [(cterm_of sg Pvar, cterm_of sg
 16.1347                              (lambda w (HOLogic.imp$HOLogic.mk_eq(r,w)$C)))]
 16.1348                      induct;
 16.1349          in standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
 16.1350 @@ -1468,26 +1458,26 @@
 16.1351  
 16.1352      val cases_prf = quick_and_dirty_prf cases_prf_noopt cases_prf_opt;
 16.1353      val cases = timeit_msg "record extension cases proof:" cases_prf;
 16.1354 -   
 16.1355 -    fun dest_convs_prf () = map (prove_simp false 
 16.1356 +
 16.1357 +    fun dest_convs_prf () = map (prove_simp false
 16.1358                        ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props;
 16.1359      val dest_convs = timeit_msg "record extension dest_convs proof:" dest_convs_prf;
 16.1360      fun dest_convs_standard_prf () = map standard dest_convs;
 16.1361 - 
 16.1362 -    val dest_convs_standard = 
 16.1363 -	timeit_msg "record extension dest_convs_standard proof:" dest_convs_standard_prf;
 16.1364  
 16.1365 -    fun upd_convs_prf_noopt () = map (prove_simp true (dest_convs_standard@upd_defs)) 
 16.1366 +    val dest_convs_standard =
 16.1367 +        timeit_msg "record extension dest_convs_standard proof:" dest_convs_standard_prf;
 16.1368 +
 16.1369 +    fun upd_convs_prf_noopt () = map (prove_simp true (dest_convs_standard@upd_defs))
 16.1370                                         upd_conv_props;
 16.1371      fun upd_convs_prf_opt () =
 16.1372 -      let 
 16.1373 +      let
 16.1374          val sg = sign_of defs_thy;
 16.1375 -        fun mkrefl (c,T) = Thm.reflexive 
 16.1376 -                            (cterm_of sg (Free (variant variants (base c ^ "'"),T))); 
 16.1377 +        fun mkrefl (c,T) = Thm.reflexive
 16.1378 +                            (cterm_of sg (Free (variant variants (base c ^ "'"),T)));
 16.1379          val refls = map mkrefl fields_more;
 16.1380          val constr_refl = Thm.reflexive (cterm_of sg (head_of ext));
 16.1381          val dest_convs' = map mk_meta_eq dest_convs;
 16.1382 -         
 16.1383 +
 16.1384          fun mkthm (udef,(fld_refl,thms)) =
 16.1385            let val bdyeq = Library.foldl (uncurry Thm.combination) (constr_refl,thms);
 16.1386                 (* (|N=N (|N=N,M=M,K=K,more=more|)
 16.1387 @@ -1498,19 +1488,19 @@
 16.1388                  *)
 16.1389                val (_$(_$v$r)$_) = prop_of udef;
 16.1390                val (_$v'$_) = prop_of fld_refl;
 16.1391 -              val udef' = cterm_instantiate 
 16.1392 +              val udef' = cterm_instantiate
 16.1393                              [(cterm_of sg v,cterm_of sg v'),
 16.1394                               (cterm_of sg r,cterm_of sg ext)] udef;
 16.1395 -	  in  standard (Thm.transitive udef' bdyeq) end;
 16.1396 -      in map mkthm (rev upd_defs  ~~ (mixit dest_convs' refls)) 
 16.1397 +          in  standard (Thm.transitive udef' bdyeq) end;
 16.1398 +      in map mkthm (rev upd_defs  ~~ (mixit dest_convs' refls))
 16.1399           handle e => print_exn e end;
 16.1400 -    
 16.1401 +
 16.1402      val upd_convs_prf = quick_and_dirty_prf upd_convs_prf_noopt upd_convs_prf_opt;
 16.1403  
 16.1404 -    val upd_convs = 
 16.1405 -	 timeit_msg "record extension upd_convs proof:" upd_convs_prf;
 16.1406 +    val upd_convs =
 16.1407 +         timeit_msg "record extension upd_convs proof:" upd_convs_prf;
 16.1408  
 16.1409 -    fun surjective_prf () = 
 16.1410 +    fun surjective_prf () =
 16.1411        prove_standard [] surjective_prop (fn prems =>
 16.1412            (EVERY [try_param_tac rN induct 1,
 16.1413                    simp_tac (HOL_basic_ss addsimps dest_convs_standard) 1]));
 16.1414 @@ -1527,42 +1517,42 @@
 16.1415  
 16.1416      val (thm_thy,([inject',induct',cases',surjective',split_meta'],
 16.1417                    [dest_convs',upd_convs'])) =
 16.1418 -      defs_thy 
 16.1419 -      |> (PureThy.add_thms o map Thm.no_attributes) 
 16.1420 +      defs_thy
 16.1421 +      |> (PureThy.add_thms o map Thm.no_attributes)
 16.1422             [("ext_inject", inject),
 16.1423              ("ext_induct", induct),
 16.1424              ("ext_cases", cases),
 16.1425              ("ext_surjective", surjective),
 16.1426              ("ext_split", split_meta)]
 16.1427        |>>> (PureThy.add_thmss o map Thm.no_attributes)
 16.1428 -              [("dest_convs",dest_convs_standard),("upd_convs",upd_convs)] 
 16.1429 +              [("dest_convs",dest_convs_standard),("upd_convs",upd_convs)]
 16.1430  
 16.1431    in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs')
 16.1432    end;
 16.1433 -   
 16.1434 +
 16.1435  fun chunks []      []   = []
 16.1436    | chunks []      xs   = [xs]
 16.1437    | chunks (l::ls) xs  = Library.take (l,xs)::chunks ls (Library.drop (l,xs));
 16.1438 - 
 16.1439 +
 16.1440  fun chop_last [] = error "last: list should not be empty"
 16.1441    | chop_last [x] = ([],x)
 16.1442    | chop_last (x::xs) = let val (tl,l) = chop_last xs in (x::tl,l) end;
 16.1443 -     	
 16.1444 +
 16.1445  fun subst_last s []      = error "subst_last: list should not be empty"
 16.1446    | subst_last s ([x])   = [s]
 16.1447    | subst_last s (x::xs) = (x::subst_last s xs);
 16.1448  
 16.1449  (* mk_recordT builds up the record type from the current extension tpye extT and a list
 16.1450 - * of parent extensions, starting with the root of the record hierarchy 
 16.1451 -*) 
 16.1452 -fun mk_recordT extT parent_exts = 
 16.1453 + * of parent extensions, starting with the root of the record hierarchy
 16.1454 +*)
 16.1455 +fun mk_recordT extT parent_exts =
 16.1456      foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) extT parent_exts;
 16.1457  
 16.1458  
 16.1459  
 16.1460  fun obj_to_meta_all thm =
 16.1461    let
 16.1462 -    fun E thm = case (SOME (spec OF [thm]) handle THM _ => NONE) of 
 16.1463 +    fun E thm = case (SOME (spec OF [thm]) handle THM _ => NONE) of
 16.1464                    SOME thm' => E thm'
 16.1465                  | NONE => thm;
 16.1466      val th1 = E thm;
 16.1467 @@ -1584,7 +1574,7 @@
 16.1468  
 16.1469  
 16.1470  (* record_definition *)
 16.1471 -fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy = 
 16.1472 +fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
 16.1473    (* smlnj needs type annotation of parents *)
 16.1474    let
 16.1475      val sign = Theory.sign_of thy;
 16.1476 @@ -1611,7 +1601,7 @@
 16.1477      val extN = full bname;
 16.1478      val types = map snd fields;
 16.1479      val alphas_fields = foldr add_typ_tfree_names [] types;
 16.1480 -    val alphas_ext = alphas inter alphas_fields; 
 16.1481 +    val alphas_ext = alphas inter alphas_fields;
 16.1482      val len = length fields;
 16.1483      val variants = variantlist (map fst bfields, moreN::rN::rN ^ "'"::wN::parent_variants);
 16.1484      val vars = ListPair.map Free (variants, types);
 16.1485 @@ -1628,7 +1618,7 @@
 16.1486      val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
 16.1487  
 16.1488  
 16.1489 -    val zeta = variant alphas "'z"; 
 16.1490 +    val zeta = variant alphas "'z";
 16.1491      val moreT = TFree (zeta, HOLogic.typeS);
 16.1492      val more = Free (moreN, moreT);
 16.1493      val full_moreN = full moreN;
 16.1494 @@ -1638,42 +1628,42 @@
 16.1495      val named_vars_more = named_vars @[(full_moreN,more)];
 16.1496      val all_vars_more = all_vars @ [more];
 16.1497      val all_named_vars_more = all_named_vars @ [(full_moreN,more)];
 16.1498 -   
 16.1499 +
 16.1500      (* 1st stage: extension_thy *)
 16.1501      val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs,ext_split,u_convs) =
 16.1502        thy
 16.1503        |> Theory.add_path bname
 16.1504        |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
 16.1505  
 16.1506 -    val _ = timing_msg "record preparing definitions";	
 16.1507 +    val _ = timing_msg "record preparing definitions";
 16.1508      val Type extension_scheme = extT;
 16.1509      val extension_name = unsuffix ext_typeN (fst extension_scheme);
 16.1510 -    val extension = let val (n,Ts) = extension_scheme in (n,subst_last HOLogic.unitT Ts) end; 
 16.1511 -    val extension_names = 
 16.1512 +    val extension = let val (n,Ts) = extension_scheme in (n,subst_last HOLogic.unitT Ts) end;
 16.1513 +    val extension_names =
 16.1514           (map ((unsuffix ext_typeN) o fst o #extension) parents) @ [extN];
 16.1515      val extension_id = Library.foldl (op ^) ("",extension_names);
 16.1516  
 16.1517 - 
 16.1518 +
 16.1519      fun rec_schemeT n = mk_recordT extT (map #extension (prune n parents));
 16.1520      val rec_schemeT0 = rec_schemeT 0;
 16.1521  
 16.1522 -    fun recT n = 
 16.1523 +    fun recT n =
 16.1524        let val (c,Ts) = extension
 16.1525        in mk_recordT (Type (c,subst_last HOLogic.unitT Ts))(map #extension (prune n parents))
 16.1526        end;
 16.1527      val recT0 = recT 0;
 16.1528 -    
 16.1529 +
 16.1530      fun mk_rec args n =
 16.1531        let val (args',more) = chop_last args;
 16.1532 -	  fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]);
 16.1533 -          fun build Ts = 
 16.1534 +          fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]);
 16.1535 +          fun build Ts =
 16.1536             foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')))
 16.1537 -      in 
 16.1538 -        if more = HOLogic.unit 
 16.1539 -        then build (map recT (0 upto parent_len)) 
 16.1540 +      in
 16.1541 +        if more = HOLogic.unit
 16.1542 +        then build (map recT (0 upto parent_len))
 16.1543          else build (map rec_schemeT (0 upto parent_len))
 16.1544        end;
 16.1545 -   
 16.1546 +
 16.1547      val r_rec0 = mk_rec all_vars_more 0;
 16.1548      val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0;
 16.1549  
 16.1550 @@ -1704,66 +1694,66 @@
 16.1551        in map (gen_record_type_tr') trnames
 16.1552        end;
 16.1553  
 16.1554 -    
 16.1555 +
 16.1556      (* prepare declarations *)
 16.1557  
 16.1558      val sel_decls = map (mk_selC rec_schemeT0) bfields_more;
 16.1559      val upd_decls = map (mk_updC updateN rec_schemeT0) bfields_more;
 16.1560      val make_decl = (makeN, all_types ---> recT0);
 16.1561 -    val fields_decl = (fields_selN, types ---> Type extension); 
 16.1562 +    val fields_decl = (fields_selN, types ---> Type extension);
 16.1563      val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
 16.1564      val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
 16.1565  
 16.1566      (* prepare definitions *)
 16.1567 -    
 16.1568 -    fun parent_more s = 
 16.1569 -         if null parents then s 
 16.1570 +
 16.1571 +    fun parent_more s =
 16.1572 +         if null parents then s
 16.1573           else mk_sel s (NameSpace.qualified (#name (List.last parents)) moreN, extT);
 16.1574  
 16.1575      fun parent_more_upd v s =
 16.1576 -      if null parents then v 
 16.1577 +      if null parents then v
 16.1578        else let val mp = NameSpace.qualified (#name (List.last parents)) moreN;
 16.1579             in mk_upd updateN mp v s end;
 16.1580 -   
 16.1581 +
 16.1582      (*record (scheme) type abbreviation*)
 16.1583      val recordT_specs =
 16.1584        [(suffix schemeN bname, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
 16.1585 -        (bname, alphas, recT0, Syntax.NoSyn)];	
 16.1586 +        (bname, alphas, recT0, Syntax.NoSyn)];
 16.1587  
 16.1588 -    (*selectors*) 
 16.1589 -    fun mk_sel_spec (c,T) = 
 16.1590 -	 Const (mk_selC rec_schemeT0 (c,T)) 
 16.1591 +    (*selectors*)
 16.1592 +    fun mk_sel_spec (c,T) =
 16.1593 +         Const (mk_selC rec_schemeT0 (c,T))
 16.1594            :== (lambda r0 (Const (mk_selC extT (suffix ext_dest c,T))$parent_more r0));
 16.1595      val sel_specs = map mk_sel_spec fields_more;
 16.1596  
 16.1597      (*updates*)
 16.1598  
 16.1599      fun mk_upd_spec (c,T) =
 16.1600 -      let 
 16.1601 -        val new = mk_upd updN c (Free (base c,T)) (parent_more r0); 
 16.1602 +      let
 16.1603 +        val new = mk_upd updN c (Free (base c,T)) (parent_more r0);
 16.1604        in Const (mk_updC updateN rec_schemeT0 (c,T))$(Free (base c,T))$r0
 16.1605            :== (parent_more_upd new r0)
 16.1606        end;
 16.1607 -    val upd_specs = map mk_upd_spec fields_more; 
 16.1608 +    val upd_specs = map mk_upd_spec fields_more;
 16.1609  
 16.1610      (*derived operations*)
 16.1611      val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :==
 16.1612        mk_rec (all_vars @ [HOLogic.unit]) 0;
 16.1613      val fields_spec = Const (full fields_selN, types ---> Type extension) $$ vars :==
 16.1614        mk_rec (all_vars @ [HOLogic.unit]) parent_len;
 16.1615 -    val extend_spec = 
 16.1616 +    val extend_spec =
 16.1617        Const (full extendN, recT0-->moreT-->rec_schemeT0) $ r_unit0 $ more :==
 16.1618        mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
 16.1619      val truncate_spec = Const (full truncateN, rec_schemeT0 --> recT0) $ r0 :==
 16.1620        mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
 16.1621  
 16.1622      (* 2st stage: defs_thy *)
 16.1623 - 
 16.1624 +
 16.1625      fun mk_defs () =
 16.1626        extension_thy
 16.1627 -        |> Theory.add_trfuns 
 16.1628 +        |> Theory.add_trfuns
 16.1629              ([],[],field_tr's, [])
 16.1630 -        |> Theory.add_advanced_trfuns 
 16.1631 +        |> Theory.add_advanced_trfuns
 16.1632              ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
 16.1633  
 16.1634          |> Theory.parent_path
 16.1635 @@ -1771,30 +1761,30 @@
 16.1636          |> Theory.add_path bname
 16.1637          |> Theory.add_consts_i
 16.1638              (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
 16.1639 -        |> (Theory.add_consts_i o map Syntax.no_syn) 
 16.1640 +        |> (Theory.add_consts_i o map Syntax.no_syn)
 16.1641              (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
 16.1642          |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs
 16.1643          |>>> (PureThy.add_defs_i false o map Thm.no_attributes) upd_specs
 16.1644 -	|>>> (PureThy.add_defs_i false o map Thm.no_attributes)
 16.1645 +        |>>> (PureThy.add_defs_i false o map Thm.no_attributes)
 16.1646                 [make_spec, fields_spec, extend_spec, truncate_spec]
 16.1647      val (defs_thy,((sel_defs,upd_defs),derived_defs)) =
 16.1648          timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
 16.1649           mk_defs;
 16.1650 -        
 16.1651 +
 16.1652  
 16.1653      (* prepare propositions *)
 16.1654 -    val _ = timing_msg "record preparing propositions";	
 16.1655 +    val _ = timing_msg "record preparing propositions";
 16.1656      val P = Free (variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
 16.1657 -    val C = Free (variant all_variants "C", HOLogic.boolT);    
 16.1658 +    val C = Free (variant all_variants "C", HOLogic.boolT);
 16.1659      val P_unit = Free (variant all_variants "P", recT0-->HOLogic.boolT);
 16.1660  
 16.1661 -    (*selectors*) 
 16.1662 +    (*selectors*)
 16.1663      val sel_conv_props =
 16.1664         map (fn (c, x as Free (_,T)) => mk_sel r_rec0 (c,T) === x) named_vars_more;
 16.1665  
 16.1666 -    (*updates*) 
 16.1667 +    (*updates*)
 16.1668      fun mk_upd_prop (i,(c,T)) =
 16.1669 -      let val x' = Free (variant all_variants (base c ^ "'"),T) 
 16.1670 +      let val x' = Free (variant all_variants (base c ^ "'"),T)
 16.1671            val args' = nth_update x' (parent_fields_len + i, all_vars_more)
 16.1672        in mk_upd updateN c x' r_rec0 === mk_rec args' 0  end;
 16.1673      val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
 16.1674 @@ -1802,7 +1792,7 @@
 16.1675      (*induct*)
 16.1676      val induct_scheme_prop =
 16.1677        All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
 16.1678 -    val induct_prop =  
 16.1679 +    val induct_prop =
 16.1680        (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
 16.1681         Trueprop (P_unit $ r_unit0));
 16.1682  
 16.1683 @@ -1810,24 +1800,24 @@
 16.1684      val surjective_prop =
 16.1685        let val args = map (fn (c,Free (_,T)) => mk_sel r0 (c,T)) all_named_vars_more
 16.1686        in r0 === mk_rec args 0 end;
 16.1687 -	
 16.1688 +
 16.1689      (*cases*)
 16.1690      val cases_scheme_prop =
 16.1691 -      (All (map dest_Free all_vars_more) 
 16.1692 -        (Trueprop (HOLogic.mk_eq (r0,r_rec0)) ==> Trueprop C)) 
 16.1693 +      (All (map dest_Free all_vars_more)
 16.1694 +        (Trueprop (HOLogic.mk_eq (r0,r_rec0)) ==> Trueprop C))
 16.1695        ==> Trueprop C;
 16.1696  
 16.1697      val cases_prop =
 16.1698 -      (All (map dest_Free all_vars) 
 16.1699 -        (Trueprop (HOLogic.mk_eq (r_unit0,r_rec_unit0)) ==> Trueprop C)) 
 16.1700 +      (All (map dest_Free all_vars)
 16.1701 +        (Trueprop (HOLogic.mk_eq (r_unit0,r_rec_unit0)) ==> Trueprop C))
 16.1702         ==> Trueprop C;
 16.1703  
 16.1704      (*split*)
 16.1705      val split_meta_prop =
 16.1706        let val P = Free (variant all_variants "P", rec_schemeT0-->Term.propT) in
 16.1707 -        Logic.mk_equals 
 16.1708 +        Logic.mk_equals
 16.1709           (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
 16.1710 -      end; 
 16.1711 +      end;
 16.1712  
 16.1713      val split_object_prop =
 16.1714        let fun ALL vs t = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) t vs
 16.1715 @@ -1842,9 +1832,9 @@
 16.1716  
 16.1717      (*equality*)
 16.1718      val equality_prop =
 16.1719 -      let 
 16.1720 -	val s' = Free (rN ^ "'", rec_schemeT0)
 16.1721 -        fun mk_sel_eq (c,Free (_,T)) =  mk_sel r0 (c,T) === mk_sel s' (c,T) 
 16.1722 +      let
 16.1723 +        val s' = Free (rN ^ "'", rec_schemeT0)
 16.1724 +        fun mk_sel_eq (c,Free (_,T)) =  mk_sel r0 (c,T) === mk_sel s' (c,T)
 16.1725          val seleqs = map mk_sel_eq all_named_vars_more
 16.1726        in All (map dest_Free [r0,s']) (Logic.list_implies (seleqs,r0 === s')) end;
 16.1727  
 16.1728 @@ -1852,29 +1842,29 @@
 16.1729  
 16.1730      fun prove stndrd = quick_and_dirty_prove stndrd (Theory.sign_of defs_thy);
 16.1731      val prove_standard = quick_and_dirty_prove true (Theory.sign_of defs_thy);
 16.1732 -    
 16.1733 +
 16.1734      fun prove_simp stndrd ss simps =
 16.1735        let val tac = simp_all_tac ss simps
 16.1736        in fn prop => prove stndrd [] prop (K tac) end;
 16.1737  
 16.1738      val ss = get_simpset (sign_of defs_thy);
 16.1739  
 16.1740 -    fun sel_convs_prf () = map (prove_simp false ss 
 16.1741 +    fun sel_convs_prf () = map (prove_simp false ss
 16.1742                             (sel_defs@ext_dest_convs)) sel_conv_props;
 16.1743      val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
 16.1744      fun sel_convs_standard_prf () = map standard sel_convs
 16.1745 -    val sel_convs_standard = 
 16.1746 -	  timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
 16.1747 +    val sel_convs_standard =
 16.1748 +          timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
 16.1749  
 16.1750 -    fun upd_convs_prf () = 
 16.1751 -	  map (prove_simp true ss (upd_defs@u_convs)) upd_conv_props;
 16.1752 -    
 16.1753 +    fun upd_convs_prf () =
 16.1754 +          map (prove_simp true ss (upd_defs@u_convs)) upd_conv_props;
 16.1755 +
 16.1756      val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
 16.1757  
 16.1758      val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
 16.1759  
 16.1760      fun induct_scheme_prf () = prove_standard [] induct_scheme_prop (fn prems =>
 16.1761 -          (EVERY [if null parent_induct 
 16.1762 +          (EVERY [if null parent_induct
 16.1763                    then all_tac else try_param_tac rN (hd parent_induct) 1,
 16.1764                    try_param_tac rN ext_induct 1,
 16.1765                    asm_simp_tac HOL_basic_ss 1]));
 16.1766 @@ -1890,18 +1880,18 @@
 16.1767        end;
 16.1768      val induct = timeit_msg "record induct proof:" induct_prf;
 16.1769  
 16.1770 -    fun surjective_prf () = 
 16.1771 +    fun surjective_prf () =
 16.1772        prove_standard [] surjective_prop (fn prems =>
 16.1773            (EVERY [try_param_tac rN induct_scheme 1,
 16.1774                    simp_tac (ss addsimps sel_convs_standard) 1]))
 16.1775      val surjective = timeit_msg "record surjective proof:" surjective_prf;
 16.1776  
 16.1777      fun cases_scheme_prf_opt () =
 16.1778 -      let 
 16.1779 +      let
 16.1780          val sg = (sign_of defs_thy);
 16.1781          val (_$(Pvar$_)) = concl_of induct_scheme;
 16.1782 -        val ind = cterm_instantiate 
 16.1783 -                    [(cterm_of sg Pvar, cterm_of sg 
 16.1784 +        val ind = cterm_instantiate
 16.1785 +                    [(cterm_of sg Pvar, cterm_of sg
 16.1786                              (lambda w (HOLogic.imp$HOLogic.mk_eq(r0,w)$C)))]
 16.1787                      induct_scheme;
 16.1788          in standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
 16.1789 @@ -1934,38 +1924,38 @@
 16.1790      val split_meta_standard = standard split_meta;
 16.1791  
 16.1792      fun split_object_prf_opt () =
 16.1793 -      let 
 16.1794 +      let
 16.1795          val sg = sign_of defs_thy;
 16.1796          val cPI= cterm_of sg (lambda r0 (Trueprop (P$r0)));
 16.1797          val (_$Abs(_,_,P$_)) = fst (Logic.dest_equals (concl_of split_meta_standard));
 16.1798          val cP = cterm_of sg P;
 16.1799          val split_meta' = cterm_instantiate [(cP,cPI)] split_meta_standard;
 16.1800          val (l,r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
 16.1801 -        val cl = cterm_of sg (HOLogic.mk_Trueprop l); 
 16.1802 -        val cr = cterm_of sg (HOLogic.mk_Trueprop r); 
 16.1803 +        val cl = cterm_of sg (HOLogic.mk_Trueprop l);
 16.1804 +        val cr = cterm_of sg (HOLogic.mk_Trueprop r);
 16.1805          val thl = assume cl                 (*All r. P r*) (* 1 *)
 16.1806                  |> obj_to_meta_all          (*!!r. P r*)
 16.1807 -                |> equal_elim split_meta'   (*!!n m more. P (ext n m more)*)  
 16.1808 -                |> meta_to_obj_all          (*All n m more. P (ext n m more)*) (* 2*) 
 16.1809 +                |> equal_elim split_meta'   (*!!n m more. P (ext n m more)*)
 16.1810 +                |> meta_to_obj_all          (*All n m more. P (ext n m more)*) (* 2*)
 16.1811                  |> implies_intr cl          (* 1 ==> 2 *)
 16.1812          val thr = assume cr                           (*All n m more. P (ext n m more)*)
 16.1813                  |> obj_to_meta_all                    (*!!n m more. P (ext n m more)*)
 16.1814 -                |> equal_elim (symmetric split_meta') (*!!r. P r*) 
 16.1815 +                |> equal_elim (symmetric split_meta') (*!!r. P r*)
 16.1816                  |> meta_to_obj_all                    (*All r. P r*)
 16.1817                  |> implies_intr cr                    (* 2 ==> 1 *)
 16.1818 -     in standard (thr COMP (thl COMP iffI)) end;   
 16.1819 +     in standard (thr COMP (thl COMP iffI)) end;
 16.1820  
 16.1821      fun split_object_prf_noopt () =
 16.1822          prove_standard [] split_object_prop (fn prems =>
 16.1823 -         EVERY [rtac iffI 1, 
 16.1824 +         EVERY [rtac iffI 1,
 16.1825                  REPEAT (rtac allI 1), etac allE 1, atac 1,
 16.1826                  rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
 16.1827  
 16.1828 -    val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt;  
 16.1829 +    val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt;
 16.1830      val split_object = timeit_msg "record split_object proof:" split_object_prf;
 16.1831  
 16.1832  
 16.1833 -    fun split_ex_prf () = 
 16.1834 +    fun split_ex_prf () =
 16.1835          prove_standard [] split_ex_prop (fn prems =>
 16.1836            EVERY [rtac iffI 1,
 16.1837                     etac exE 1,
 16.1838 @@ -1978,19 +1968,19 @@
 16.1839                   atac 1]);
 16.1840      val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
 16.1841  
 16.1842 -    fun equality_tac thms = 
 16.1843 +    fun equality_tac thms =
 16.1844        let val (s'::s::eqs) = rev thms;
 16.1845            val ss' = ss addsimps (s'::s::sel_convs_standard);
 16.1846            val eqs' = map (simplify ss') eqs;
 16.1847        in simp_tac (HOL_basic_ss addsimps (s'::s::eqs')) 1 end;
 16.1848 - 
 16.1849 +
 16.1850     fun equality_prf () = prove_standard [] equality_prop (fn _ =>
 16.1851        fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
 16.1852          st |> (res_inst_tac [(rN, s)] cases_scheme 1
 16.1853          THEN res_inst_tac [(rN, s')] cases_scheme 1
 16.1854 -        THEN (METAHYPS equality_tac 1)) 
 16.1855 +        THEN (METAHYPS equality_tac 1))
 16.1856               (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
 16.1857 -      end);                              
 16.1858 +      end);
 16.1859       val equality = timeit_msg "record equality proof:" equality_prf;
 16.1860  
 16.1861      val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],
 16.1862 @@ -2007,7 +1997,7 @@
 16.1863        |>>> (PureThy.add_thms o map Thm.no_attributes)
 16.1864            [("surjective", surjective),
 16.1865             ("equality", equality)]
 16.1866 -      |>>> PureThy.add_thms 
 16.1867 +      |>>> PureThy.add_thms
 16.1868          [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
 16.1869           (("induct", induct), induct_type_global name),
 16.1870           (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
 16.1871 @@ -2021,14 +2011,14 @@
 16.1872        |> (#1 oo PureThy.add_thmss)
 16.1873            [(("simps", sel_upd_simps), [Simplifier.simp_add_global]),
 16.1874             (("iffs",iffs), [iff_add_global])]
 16.1875 -      |> put_record name (make_record_info args parent fields extension induct_scheme') 
 16.1876 +      |> put_record name (make_record_info args parent fields extension induct_scheme')
 16.1877        |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
 16.1878        |> add_record_equalities extension_id equality'
 16.1879        |> add_extinjects ext_inject
 16.1880        |> add_extsplit extension_name ext_split
 16.1881        |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme')
 16.1882 -      |> add_extfields extension_name (fields @ [(full_moreN,moreT)]) 
 16.1883 -      |> add_fieldext (extension_name,snd extension) (names @ [full_moreN]) 
 16.1884 +      |> add_extfields extension_name (fields @ [(full_moreN,moreT)])
 16.1885 +      |> add_fieldext (extension_name,snd extension) (names @ [full_moreN])
 16.1886        |> Theory.parent_path;
 16.1887  
 16.1888    in final_thy
 16.1889 @@ -2040,7 +2030,7 @@
 16.1890    work to record_definition*)
 16.1891  fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
 16.1892    let
 16.1893 -    val _ = Theory.requires thy "Record" "record definitions"; 
 16.1894 +    val _ = Theory.requires thy "Record" "record definitions";
 16.1895      val sign = Theory.sign_of thy;
 16.1896      val _ = message ("Defining record " ^ quote bname ^ " ...");
 16.1897  
 16.1898 @@ -2079,7 +2069,7 @@
 16.1899      (* errors *)
 16.1900  
 16.1901      val name = Sign.full_name sign bname;
 16.1902 -    val err_dup_record =  
 16.1903 +    val err_dup_record =
 16.1904        if is_none (get_record thy name) then []
 16.1905        else ["Duplicate definition of record " ^ quote name];
 16.1906  
 16.1907 @@ -2126,7 +2116,7 @@
 16.1908  val setup =
 16.1909   [RecordsData.init,
 16.1910    Theory.add_trfuns ([], parse_translation, [], []),
 16.1911 -  Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),    
 16.1912 +  Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),
 16.1913    Simplifier.change_simpset_of Simplifier.addsimprocs
 16.1914      [record_simproc, record_upd_simproc, record_eq_simproc]];
 16.1915  
 16.1916 @@ -2139,8 +2129,8 @@
 16.1917      (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
 16.1918  
 16.1919  val recordP =
 16.1920 -  OuterSyntax.command "record" "define extensible record" K.thy_decl   
 16.1921 -    (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));  
 16.1922 +  OuterSyntax.command "record" "define extensible record" K.thy_decl
 16.1923 +    (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
 16.1924  
 16.1925  val _ = OuterSyntax.add_parsers [recordP];
 16.1926  
 16.1927 @@ -2150,4 +2140,4 @@
 16.1928  
 16.1929  
 16.1930  structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage;
 16.1931 -open BasicRecordPackage;   
 16.1932 +open BasicRecordPackage;
    17.1 --- a/src/HOL/Tools/refute.ML	Mon Sep 05 17:38:17 2005 +0200
    17.2 +++ b/src/HOL/Tools/refute.ML	Mon Sep 05 17:38:18 2005 +0200
    17.3 @@ -298,11 +298,11 @@
    17.4  	let
    17.5  		val {interpreters, printers, parameters} = RefuteData.get thy
    17.6  	in
    17.7 -		case Symtab.lookup (parameters, name) of
    17.8 +		case Symtab.curried_lookup parameters name of
    17.9  		  NONE   => RefuteData.put
   17.10  			{interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy
   17.11  		| SOME _ => RefuteData.put
   17.12 -			{interpreters = interpreters, printers = printers, parameters = Symtab.update ((name, value), parameters)} thy
   17.13 +			{interpreters = interpreters, printers = printers, parameters = Symtab.curried_update (name, value) parameters} thy
   17.14  	end;
   17.15  
   17.16  (* ------------------------------------------------------------------------- *)
   17.17 @@ -312,7 +312,7 @@
   17.18  
   17.19  	(* theory -> string -> string option *)
   17.20  
   17.21 -	fun get_default_param thy name = Symtab.lookup ((#parameters o RefuteData.get) thy, name);
   17.22 +	val get_default_param = Symtab.curried_lookup o #parameters o RefuteData.get;
   17.23  
   17.24  (* ------------------------------------------------------------------------- *)
   17.25  (* get_default_params: returns a list of all '(name, value)' pairs that are  *)
   17.26 @@ -321,7 +321,7 @@
   17.27  
   17.28  	(* theory -> (string * string) list *)
   17.29  
   17.30 -	fun get_default_params thy = (Symtab.dest o #parameters o RefuteData.get) thy;
   17.31 +	val get_default_params = Symtab.dest o #parameters o RefuteData.get;
   17.32  
   17.33  (* ------------------------------------------------------------------------- *)
   17.34  (* actual_params: takes a (possibly empty) list 'params' of parameters that  *)
    18.1 --- a/src/HOL/Tools/res_axioms.ML	Mon Sep 05 17:38:17 2005 +0200
    18.2 +++ b/src/HOL/Tools/res_axioms.ML	Mon Sep 05 17:38:18 2005 +0200
    18.3 @@ -257,7 +257,7 @@
    18.4  (*Populate the clause cache using the supplied theorems*)
    18.5  fun skolemlist [] thy = thy
    18.6    | skolemlist ((name,th)::nths) thy = 
    18.7 -      (case Symtab.lookup (!clause_cache,name) of
    18.8 +      (case Symtab.curried_lookup (!clause_cache) name of
    18.9  	  NONE => 
   18.10  	    let val (nnfth,ok) = (to_nnf thy th, true)  
   18.11  	                 handle THM _ => (asm_rl, false)
   18.12 @@ -265,8 +265,7 @@
   18.13                  if ok then
   18.14                      let val (skoths,thy') = skolem thy (name, nnfth)
   18.15  			val cls = Meson.make_cnf skoths nnfth
   18.16 -		    in  clause_cache := 
   18.17 -		     	  Symtab.update ((name, (th,cls)), !clause_cache);
   18.18 +		    in change clause_cache (Symtab.curried_update (name, (th, cls)));
   18.19  			skolemlist nths thy'
   18.20  		    end
   18.21  		else skolemlist nths thy
   18.22 @@ -277,17 +276,15 @@
   18.23  fun cnf_axiom (name,th) =
   18.24      case name of
   18.25  	  "" => cnf_axiom_aux th (*no name, so can't cache*)
   18.26 -	| s  => case Symtab.lookup (!clause_cache,s) of
   18.27 +	| s  => case Symtab.curried_lookup (!clause_cache) s of
   18.28  	  	  NONE => 
   18.29  		    let val cls = cnf_axiom_aux th
   18.30 -		    in  clause_cache := Symtab.update ((s, (th,cls)), !clause_cache); cls
   18.31 -		    end
   18.32 +		    in change clause_cache (Symtab.curried_update (s, (th, cls))); cls end
   18.33  	        | SOME(th',cls) =>
   18.34  		    if eq_thm(th,th') then cls
   18.35  		    else (*New theorem stored under the same name? Possible??*)
   18.36  		      let val cls = cnf_axiom_aux th
   18.37 -		      in  clause_cache := Symtab.update ((s, (th,cls)), !clause_cache); cls
   18.38 -		      end;
   18.39 +		      in change clause_cache (Symtab.curried_update (s, (th, cls))); cls end;
   18.40  
   18.41  fun pairname th = (Thm.name_of_thm th, th);
   18.42  
    19.1 --- a/src/HOL/Tools/res_clause.ML	Mon Sep 05 17:38:17 2005 +0200
    19.2 +++ b/src/HOL/Tools/res_clause.ML	Mon Sep 05 17:38:18 2005 +0200
    19.3 @@ -136,16 +136,16 @@
    19.4  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
    19.5  
    19.6  fun make_fixed_const c =
    19.7 -    case Symtab.lookup (const_trans_table,c) of
    19.8 +    case Symtab.curried_lookup const_trans_table c of
    19.9          SOME c' => c'
   19.10 -      | NONE =>  const_prefix ^ (ascii_of c);
   19.11 +      | NONE =>  const_prefix ^ ascii_of c;
   19.12  
   19.13  fun make_fixed_type_const c = 
   19.14 -    case Symtab.lookup (type_const_trans_table,c) of
   19.15 +    case Symtab.curried_lookup type_const_trans_table c of
   19.16          SOME c' => c'
   19.17 -      | NONE =>  tconst_prefix ^ (ascii_of c);
   19.18 +      | NONE =>  tconst_prefix ^ ascii_of c;
   19.19  
   19.20 -fun make_type_class clas = class_prefix ^ (ascii_of clas);
   19.21 +fun make_type_class clas = class_prefix ^ ascii_of clas;
   19.22  
   19.23  
   19.24  
    20.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Sep 05 17:38:17 2005 +0200
    20.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Sep 05 17:38:18 2005 +0200
    20.3 @@ -62,9 +62,8 @@
    20.4  end);
    20.5  
    20.6  fun put_typedef newT oldT Abs_name Rep_name thy =
    20.7 -  TypedefData.put (Symtab.update_new
    20.8 -    ((fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)),
    20.9 -     TypedefData.get thy)) thy;
   20.10 +  TypedefData.put (Symtab.curried_update_new
   20.11 +    (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)) (TypedefData.get thy)) thy;
   20.12  
   20.13  
   20.14  
   20.15 @@ -283,8 +282,10 @@
   20.16            foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
   20.17          val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
   20.18        in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
   20.19 -    fun lookup f T = getOpt (Option.map f (Symtab.lookup
   20.20 -      (TypedefData.get thy, get_name T)), "")
   20.21 +    fun lookup f T =
   20.22 +      (case Symtab.curried_lookup (TypedefData.get thy) (get_name T) of
   20.23 +        NONE => ""
   20.24 +      | SOME s => f s);
   20.25    in
   20.26      (case strip_comb t of
   20.27         (Const (s, Type ("fun", [T, U])), ts) =>
   20.28 @@ -303,7 +304,7 @@
   20.29    | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
   20.30  
   20.31  fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
   20.32 -      (case Symtab.lookup (TypedefData.get thy, s) of
   20.33 +      (case Symtab.curried_lookup (TypedefData.get thy) s of
   20.34           NONE => NONE
   20.35         | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
   20.36             if isSome (Codegen.get_assoc_type thy tname) then NONE else
    21.1 --- a/src/Pure/codegen.ML	Mon Sep 05 17:38:17 2005 +0200
    21.2 +++ b/src/Pure/codegen.ML	Mon Sep 05 17:38:18 2005 +0200
    21.3 @@ -427,12 +427,13 @@
    21.4            let
    21.5              val s' = NameSpace.pack ys
    21.6              val s'' = NameSpace.append module s'
    21.7 -          in case Symtab.lookup (used, s'') of
    21.8 -              NONE => ((module, s'), (Symtab.update_new ((s, (module, s')), tab),
    21.9 -                Symtab.update_new ((s'', ()), used)))
   21.10 +          in case Symtab.curried_lookup used s'' of
   21.11 +              NONE => ((module, s'),
   21.12 +                (Symtab.curried_update_new (s, (module, s')) tab,
   21.13 +                 Symtab.curried_update_new (s'', ()) used))
   21.14              | SOME _ => find_name yss
   21.15            end
   21.16 -  in case Symtab.lookup (tab, s) of
   21.17 +  in case Symtab.curried_lookup tab s of
   21.18        NONE => find_name (Library.suffixes1 (NameSpace.unpack s))
   21.19      | SOME name => (name, p)
   21.20    end;
   21.21 @@ -452,7 +453,7 @@
   21.22    in ((gr, (tab1', tab2)), (module, s'')) end;
   21.23  
   21.24  fun get_const_id cname (gr, (tab1, tab2)) =
   21.25 -  case Symtab.lookup (fst tab1, cname) of
   21.26 +  case Symtab.curried_lookup (fst tab1) cname of
   21.27      NONE => error ("get_const_id: no such constant: " ^ quote cname)
   21.28    | SOME (module, s) =>
   21.29        let
   21.30 @@ -468,7 +469,7 @@
   21.31    in ((gr, (tab1, tab2')), (module, s'')) end;
   21.32  
   21.33  fun get_type_id tyname (gr, (tab1, tab2)) =
   21.34 -  case Symtab.lookup (fst tab2, tyname) of
   21.35 +  case Symtab.curried_lookup (fst tab2) tyname of
   21.36      NONE => error ("get_type_id: no such type: " ^ quote tyname)
   21.37    | SOME (module, s) =>
   21.38        let
   21.39 @@ -556,15 +557,15 @@
   21.40          NONE => defs
   21.41        | SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of
   21.42            NONE => defs
   21.43 -        | SOME (s, (T, (args, rhs))) => Symtab.update
   21.44 -            ((s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) ::
   21.45 -            if_none (Symtab.lookup (defs, s)) []), defs)))
   21.46 +        | SOME (s, (T, (args, rhs))) => Symtab.curried_update
   21.47 +            (s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) ::
   21.48 +            if_none (Symtab.curried_lookup defs s) []) defs))
   21.49    in
   21.50      foldl (fn ((thyname, axms), defs) =>
   21.51        Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss
   21.52    end;
   21.53  
   21.54 -fun get_defn thy defs s T = (case Symtab.lookup (defs, s) of
   21.55 +fun get_defn thy defs s T = (case Symtab.curried_lookup defs s of
   21.56      NONE => NONE
   21.57    | SOME ds =>
   21.58        let val i = find_index (is_instance thy T o fst) ds
   21.59 @@ -828,7 +829,7 @@
   21.60          (Graph.merge (fn ((_, module, _), (_, module', _)) =>
   21.61             module = module') (gr, gr'),
   21.62           (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr
   21.63 -           (map (fn s => case Symtab.lookup (graphs, s) of
   21.64 +           (map (fn s => case Symtab.curried_lookup graphs s of
   21.65                  NONE => error ("Undefined code module: " ^ s)
   21.66                | SOME gr => gr) modules))
   21.67        handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks);
   21.68 @@ -1055,8 +1056,7 @@
   21.69                     "use \"" ^ name ^ ".ML\";\n") code)) :: code)
   21.70             else File.write (Path.unpack fname) (snd (hd code)));
   21.71             if lib then thy
   21.72 -           else map_modules (fn graphs =>
   21.73 -             Symtab.update ((module, gr), graphs)) thy)
   21.74 +           else map_modules (Symtab.curried_update (module, gr)) thy)
   21.75       end));
   21.76  
   21.77  val code_libraryP =
    22.1 --- a/src/ZF/Tools/datatype_package.ML	Mon Sep 05 17:38:17 2005 +0200
    22.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon Sep 05 17:38:18 2005 +0200
    22.3 @@ -383,8 +383,8 @@
    22.4            (("recursor_eqns", recursor_eqns), []),
    22.5            (("free_iffs", free_iffs), []),
    22.6            (("free_elims", free_SEs), [])])
    22.7 -        |> DatatypesData.map (fn tab => Symtab.update ((big_rec_name, dt_info), tab))
    22.8 -        |> ConstructorsData.map (fn tab => foldr Symtab.update tab con_pairs)
    22.9 +        |> DatatypesData.map (Symtab.curried_update (big_rec_name, dt_info))
   22.10 +        |> ConstructorsData.map (fold Symtab.curried_update con_pairs)
   22.11          |> Theory.parent_path,
   22.12     ind_result,
   22.13     {con_defs = con_defs,