curried_lookup/update;
authorwenzelm
Thu Sep 01 22:15:10 2005 +0200 (2005-09-01)
changeset 17223430edc6b7826
parent 17222 819bc7f22423
child 17224 a78339014063
curried_lookup/update;
tuned;
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/extract_common_term.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/proofchecker.ML
src/Pure/Tools/compute.ML
src/Pure/defs.ML
src/ZF/Tools/induct_tacs.ML
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Thu Sep 01 18:48:54 2005 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Thu Sep 01 22:15:10 2005 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  It works by (a) massaging both sides to bring the selected term to the front:
     1.6  
     1.7 -     #m*u + (i + j) ~~ #m'*u + (i' + j') 
     1.8 +     #m*u + (i + j) ~~ #m'*u + (i' + j')
     1.9  
    1.10  (b) then using bal_add1 or bal_add2 to reach
    1.11  
    1.12 @@ -36,7 +36,7 @@
    1.13    val bal_add1: thm
    1.14    val bal_add2: thm
    1.15    (*proof tools*)
    1.16 -  val prove_conv: tactic list -> theory -> 
    1.17 +  val prove_conv: tactic list -> theory ->
    1.18                    thm list -> string list -> term * term -> thm option
    1.19    val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
    1.20    val norm_tac: simpset -> tactic                (*proves the initial lemma*)
    1.21 @@ -48,24 +48,22 @@
    1.22  functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
    1.23    sig
    1.24    val proc: theory -> simpset -> term -> thm option
    1.25 -  end 
    1.26 +  end
    1.27  =
    1.28  struct
    1.29  
    1.30  (*For t = #n*u then put u in the table*)
    1.31 -fun update_by_coeff (tab, t) =
    1.32 -  Termtab.update ((#2 (Data.dest_coeff t), ()), tab);
    1.33 +fun update_by_coeff t =
    1.34 +  Termtab.curried_update (#2 (Data.dest_coeff t), ());
    1.35  
    1.36  (*a left-to-right scan of terms1, seeking a term of the form #n*u, where
    1.37    #m*u is in terms2 for some m*)
    1.38  fun find_common (terms1,terms2) =
    1.39 -  let val tab2 = Library.foldl update_by_coeff (Termtab.empty, terms2)
    1.40 -      fun seek [] = raise TERM("find_common", []) 
    1.41 -	| seek (t::terms) =
    1.42 -	      let val (_,u) = Data.dest_coeff t 
    1.43 -	      in  if isSome (Termtab.lookup (tab2, u)) then u
    1.44 -		  else seek terms
    1.45 -	      end
    1.46 +  let val tab2 = fold update_by_coeff terms2 Termtab.empty
    1.47 +      fun seek [] = raise TERM("find_common", [])
    1.48 +        | seek (t::terms) =
    1.49 +              let val (_,u) = Data.dest_coeff t
    1.50 +              in if Termtab.defined tab2 u then u else seek terms end
    1.51    in  seek terms1 end;
    1.52  
    1.53  (*the simplification procedure*)
    1.54 @@ -74,7 +72,7 @@
    1.55        val hyps = prems_of_ss ss;
    1.56        (*first freeze any Vars in the term to prevent flex-flex problems*)
    1.57        val (t', xs) = Term.adhoc_freeze_vars t;
    1.58 -      val (t1,t2) = Data.dest_bal t' 
    1.59 +      val (t1,t2) = Data.dest_bal t'
    1.60        val terms1 = Data.dest_sum t1
    1.61        and terms2 = Data.dest_sum t2
    1.62        val u = find_common (terms1,terms2)
    1.63 @@ -83,30 +81,30 @@
    1.64        and T = Term.fastype_of u
    1.65        fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms)
    1.66        val reshape =  (*Move i*u to the front and put j*u into standard form
    1.67 -		       i + #m + j + k == #m + i + (j + k) *)
    1.68 -	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    1.69 -		raise TERM("cancel_numerals", []) 
    1.70 -	    else Data.prove_conv [Data.norm_tac ss] thy hyps xs
    1.71 -			(t', 
    1.72 -			 Data.mk_bal (newshape(n1,terms1'), 
    1.73 -				      newshape(n2,terms2')))
    1.74 +                       i + #m + j + k == #m + i + (j + k) *)
    1.75 +            if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    1.76 +                raise TERM("cancel_numerals", [])
    1.77 +            else Data.prove_conv [Data.norm_tac ss] thy hyps xs
    1.78 +                        (t',
    1.79 +                         Data.mk_bal (newshape(n1,terms1'),
    1.80 +                                      newshape(n2,terms2')))
    1.81    in
    1.82        Option.map (Data.simplify_meta_eq ss)
    1.83 -       (if n2<=n1 then 
    1.84 -	    Data.prove_conv 
    1.85 -	       [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
    1.86 -		Data.numeral_simp_tac ss] thy hyps xs
    1.87 -	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
    1.88 -				 Data.mk_sum T terms2'))
    1.89 -	else
    1.90 -	    Data.prove_conv 
    1.91 -	       [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
    1.92 -		Data.numeral_simp_tac ss] thy hyps xs
    1.93 -	       (t', Data.mk_bal (Data.mk_sum T terms1', 
    1.94 -				 newshape(n2-n1,terms2'))))
    1.95 +       (if n2<=n1 then
    1.96 +            Data.prove_conv
    1.97 +               [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
    1.98 +                Data.numeral_simp_tac ss] thy hyps xs
    1.99 +               (t', Data.mk_bal (newshape(n1-n2,terms1'),
   1.100 +                                 Data.mk_sum T terms2'))
   1.101 +        else
   1.102 +            Data.prove_conv
   1.103 +               [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
   1.104 +                Data.numeral_simp_tac ss] thy hyps xs
   1.105 +               (t', Data.mk_bal (Data.mk_sum T terms1',
   1.106 +                                 newshape(n2-n1,terms2'))))
   1.107    end
   1.108    handle TERM _ => NONE
   1.109         | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
   1.110 -			     Undeclared type constructor "Numeral.bin"*)
   1.111 +                             Undeclared type constructor "Numeral.bin"*)
   1.112  
   1.113  end;
     2.1 --- a/src/Provers/Arith/extract_common_term.ML	Thu Sep 01 18:48:54 2005 +0200
     2.2 +++ b/src/Provers/Arith/extract_common_term.ML	Thu Sep 01 22:15:10 2005 +0200
     2.3 @@ -37,12 +37,9 @@
     2.4  =
     2.5  struct
     2.6  
     2.7 -(*Store the term t in the table*)
     2.8 -fun update_by_coeff t tab = Termtab.update ((t, ()), tab);
     2.9 -
    2.10  (*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
    2.11  fun find_common (terms1,terms2) =
    2.12 -  let val tab2 = fold update_by_coeff terms2 Termtab.empty
    2.13 +  let val tab2 = fold (Termtab.curried_update o rpair ()) terms2 Termtab.empty
    2.14        fun seek [] = raise TERM("find_common", []) 
    2.15  	| seek (u::terms) =
    2.16  	      if Termtab.defined tab2 u then u
     3.1 --- a/src/Pure/Proof/extraction.ML	Thu Sep 01 18:48:54 2005 +0200
     3.2 +++ b/src/Pure/Proof/extraction.ML	Thu Sep 01 22:15:10 2005 +0200
     3.3 @@ -301,8 +301,7 @@
     3.4    in
     3.5      ExtractionData.put
     3.6        {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
     3.7 -       realizers = foldr Symtab.update_multi
     3.8 -         realizers (map (prep_rlz thy) (rev rs)),
     3.9 +       realizers = fold (Symtab.curried_update_multi o prep_rlz thy) rs realizers,
    3.10         defs = defs, expand = expand, prep = prep} thy
    3.11    end
    3.12  
    3.13 @@ -565,7 +564,7 @@
    3.14                else fst (extr d defs vs ts Ts hs prf0)
    3.15            in
    3.16              if T = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0)
    3.17 -            else case Symtab.lookup (realizers, name) of
    3.18 +            else case Symtab.curried_lookup realizers name of
    3.19                NONE => (case find vs' (find' name defs') of
    3.20                  NONE =>
    3.21                    let
    3.22 @@ -601,7 +600,7 @@
    3.23            in
    3.24              if etype_of thy' vs' [] prop = nullT andalso
    3.25                realizes_null vs' prop aconv prop then (defs, prf0)
    3.26 -            else case find vs' (Symtab.lookup_multi (realizers, s)) of
    3.27 +            else case find vs' (Symtab.curried_lookup_multi realizers s) of
    3.28                SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
    3.29              | NONE => error ("corr: no realizer for instance of axiom " ^
    3.30                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
    3.31 @@ -649,7 +648,7 @@
    3.32              val (vs', tye) = find_inst prop Ts ts vs;
    3.33              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
    3.34            in
    3.35 -            case Symtab.lookup (realizers, s) of
    3.36 +            case Symtab.curried_lookup realizers s of
    3.37                NONE => (case find vs' (find' s defs) of
    3.38                  NONE =>
    3.39                    let
    3.40 @@ -708,7 +707,7 @@
    3.41              val (vs', tye) = find_inst prop Ts ts vs;
    3.42              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
    3.43            in
    3.44 -            case find vs' (Symtab.lookup_multi (realizers, s)) of
    3.45 +            case find vs' (Symtab.curried_lookup_multi realizers s) of
    3.46                SOME (t, _) => (defs, subst_TVars tye' t)
    3.47              | NONE => error ("extr: no realizer for instance of axiom " ^
    3.48                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
     4.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu Sep 01 18:48:54 2005 +0200
     4.2 +++ b/src/Pure/Proof/proof_syntax.ML	Thu Sep 01 22:15:10 2005 +0200
     4.3 @@ -97,10 +97,10 @@
     4.4      val thms' = map (apsnd Thm.full_prop_of) (PureThy.all_thms_of thy);
     4.5  
     4.6      val tab = Symtab.foldl (fn (tab, (key, ps)) =>
     4.7 -      let val prop = getOpt (assoc_string (thms', key), Bound 0)
     4.8 +      let val prop = if_none (AList.lookup (op =) thms' key) (Bound 0)
     4.9        in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
    4.10          if prop <> prop' then
    4.11 -          (Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)
    4.12 +          (Symtab.curried_update (key ^ "_" ^ string_of_int i, prf) tab, i+1)
    4.13          else x) (tab, 1) ps)
    4.14        end) (Symtab.empty, thms);
    4.15  
    4.16 @@ -110,8 +110,8 @@
    4.17        | rename (prf % t) = rename prf % t
    4.18        | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
    4.19            let
    4.20 -            val prop' = getOpt (assoc_string (thms', s), Bound 0);
    4.21 -            val ps = map fst (valOf (Symtab.lookup (thms, s))) \ prop'
    4.22 +            val prop' = if_none (AList.lookup (op =) thms' s) (Bound 0);
    4.23 +            val ps = map fst (the (Symtab.curried_lookup thms s)) \ prop'
    4.24            in if prop = prop' then prf' else
    4.25              PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
    4.26                prf, prop, Ts)
    4.27 @@ -138,15 +138,15 @@
    4.28                 "axm" :: xs =>
    4.29                   let
    4.30                     val name = NameSpace.pack xs;
    4.31 -                   val prop = (case assoc_string (axms, name) of
    4.32 +                   val prop = (case AList.lookup (op =) axms name of
    4.33                         SOME prop => prop
    4.34                       | NONE => error ("Unknown axiom " ^ quote name))
    4.35                   in PAxm (name, prop, NONE) end
    4.36               | "thm" :: xs =>
    4.37                   let val name = NameSpace.pack xs;
    4.38 -                 in (case assoc_string (thms, name) of
    4.39 +                 in (case AList.lookup (op =) thms name of
    4.40                       SOME thm => fst (strip_combt (Thm.proof_of thm))
    4.41 -                   | NONE => (case Symtab.lookup (tab, name) of
    4.42 +                   | NONE => (case Symtab.curried_lookup tab name of
    4.43                           SOME prf => prf
    4.44                         | NONE => error ("Unknown theorem " ^ quote name)))
    4.45                   end
     5.1 --- a/src/Pure/Proof/proofchecker.ML	Thu Sep 01 18:48:54 2005 +0200
     5.2 +++ b/src/Pure/Proof/proofchecker.ML	Thu Sep 01 22:15:10 2005 +0200
     5.3 @@ -19,9 +19,9 @@
     5.4  (***** construct a theorem out of a proof term *****)
     5.5  
     5.6  fun lookup_thm thy =
     5.7 -  let val tab = fold_rev (curry Symtab.update) (PureThy.all_thms_of thy) Symtab.empty
     5.8 +  let val tab = fold_rev Symtab.curried_update (PureThy.all_thms_of thy) Symtab.empty
     5.9    in
    5.10 -    (fn s => case Symtab.lookup (tab, s) of
    5.11 +    (fn s => case Symtab.curried_lookup tab s of
    5.12         NONE => error ("Unknown theorem " ^ quote s)
    5.13       | SOME thm => thm)
    5.14    end;
     6.1 --- a/src/Pure/Tools/compute.ML	Thu Sep 01 18:48:54 2005 +0200
     6.2 +++ b/src/Pure/Tools/compute.ML	Thu Sep 01 22:15:10 2005 +0200
     6.3 @@ -44,13 +44,13 @@
     6.4  val remove_types =
     6.5      let
     6.6          fun remove_types_var table invtable ccount vcount ldepth t =
     6.7 -            (case Termtab.lookup (table, t) of
     6.8 +            (case Termtab.curried_lookup table t of
     6.9                   NONE =>
    6.10                   let
    6.11                       val a = AbstractMachine.Var vcount
    6.12                   in
    6.13 -                     (Termtab.update ((t, a), table),
    6.14 -                      AMTermTab.update ((a, t), invtable),
    6.15 +                     (Termtab.curried_update (t, a) table,
    6.16 +                      AMTermTab.curried_update (a, t) invtable,
    6.17                        ccount,
    6.18                        inc vcount,
    6.19                        AbstractMachine.Var (add vcount ldepth))
    6.20 @@ -60,13 +60,13 @@
    6.21                 | SOME _ => sys_error "remove_types_var: lookup should be a var")
    6.22  
    6.23          fun remove_types_const table invtable ccount vcount ldepth t =
    6.24 -            (case Termtab.lookup (table, t) of
    6.25 +            (case Termtab.curried_lookup table t of
    6.26                   NONE =>
    6.27                   let
    6.28                       val a = AbstractMachine.Const ccount
    6.29                   in
    6.30 -                     (Termtab.update ((t, a), table),
    6.31 -                      AMTermTab.update ((a, t), invtable),
    6.32 +                     (Termtab.curried_update (t, a) table,
    6.33 +                      AMTermTab.curried_update (a, t) invtable,
    6.34                        inc ccount,
    6.35                        vcount,
    6.36                        a)
    6.37 @@ -114,12 +114,12 @@
    6.38      let
    6.39          fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) =
    6.40              if v < ldepth then (Bound v, List.nth (bounds, v)) else
    6.41 -            (case AMTermTab.lookup (invtable, AbstractMachine.Var (v-ldepth)) of
    6.42 +            (case AMTermTab.curried_lookup invtable (AbstractMachine.Var (v-ldepth)) of
    6.43                   SOME (t as Var (_, ty)) => (t, ty)
    6.44                 | SOME (t as Free (_, ty)) => (t, ty)
    6.45                 | _ => sys_error "infer_types: lookup should deliver Var or Free")
    6.46            | infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) =
    6.47 -            (case AMTermTab.lookup (invtable, c) of
    6.48 +            (case AMTermTab.curried_lookup invtable c of
    6.49                   SOME (c as Const (_, ty)) => (c, ty)
    6.50                 | _ => sys_error "infer_types: lookup should deliver Const")
    6.51            | infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) =
    6.52 @@ -176,10 +176,10 @@
    6.53  
    6.54                  fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =
    6.55                      let
    6.56 -                        val var' = valOf (AMTermTab.lookup (invtable, var))
    6.57 +                        val var' = valOf (AMTermTab.curried_lookup invtable var)
    6.58                          val table = Termtab.delete var' table
    6.59                          val invtable = AMTermTab.delete var invtable
    6.60 -                        val vars = Inttab.update_new ((v, n), vars) handle Inttab.DUP _ =>
    6.61 +                        val vars = Inttab.curried_update_new (v, n) vars handle Inttab.DUP _ =>
    6.62                            raise (Make "no duplicate variable in pattern allowed")
    6.63                      in
    6.64                          (table, invtable, n+1, vars, AbstractMachine.PVar)
    6.65 @@ -217,7 +217,7 @@
    6.66  
    6.67                  fun rename ldepth vars (var as AbstractMachine.Var v) =
    6.68                      if v < ldepth then var
    6.69 -                    else (case Inttab.lookup (vars, v-ldepth) of
    6.70 +                    else (case Inttab.curried_lookup vars (v - ldepth) of
    6.71                                NONE => raise (Make "new variable on right hand side")
    6.72                              | SOME n => AbstractMachine.Var ((vcount-n-1)+ldepth))
    6.73                    | rename ldepth vars (c as AbstractMachine.Const _) = c
    6.74 @@ -231,14 +231,12 @@
    6.75              end
    6.76  
    6.77          val (table, invtable, ccount, rules) =
    6.78 -            List.foldl (fn (th, (table, invtable, ccount, rules)) =>
    6.79 -                           let
    6.80 -                               val (table, invtable, ccount, rule) =
    6.81 -                                   thm2rule table invtable ccount th
    6.82 -                           in
    6.83 -                               (table, invtable, ccount, rule::rules)
    6.84 -                           end)
    6.85 -                       (Termtab.empty, AMTermTab.empty, 0, []) (List.rev ths)
    6.86 +          fold_rev (fn th => fn (table, invtable, ccount, rules) =>
    6.87 +            let
    6.88 +              val (table, invtable, ccount, rule) =
    6.89 +                  thm2rule table invtable ccount th
    6.90 +            in (table, invtable, ccount, rule::rules) end)
    6.91 +          ths (Termtab.empty, AMTermTab.empty, 0, [])
    6.92  
    6.93          val prog = AbstractMachine.compile rules
    6.94  
     7.1 --- a/src/Pure/defs.ML	Thu Sep 01 18:48:54 2005 +0200
     7.2 +++ b/src/Pure/defs.ML	Thu Sep 01 22:15:10 2005 +0200
     7.3 @@ -46,13 +46,13 @@
     7.4           typ  (* type of the constant in this particular definition *)
     7.5           * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *)
     7.6  
     7.7 -fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
     7.8 +fun getnode graph = the o Symtab.curried_lookup graph
     7.9  fun get_nodedefs (Node (_, defs, _, _, _)) = defs
    7.10 -fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup (defs, defname)
    7.11 -fun get_defnode' graph noderef defname =
    7.12 -    Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
    7.13 +fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.curried_lookup defs defname
    7.14 +fun get_defnode' graph noderef =
    7.15 +  Symtab.curried_lookup (get_nodedefs (the (Symtab.curried_lookup graph noderef)))
    7.16  
    7.17 -fun table_size table = Symtab.foldl (fn (x, _) => x+1) (0, table)
    7.18 +fun table_size table = Symtab.fold (K (fn x => x + 1)) table 0;
    7.19  
    7.20  datatype graphaction =
    7.21      Declare of string * typ
    7.22 @@ -89,14 +89,14 @@
    7.23  fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2;
    7.24  
    7.25  fun subst_incr_tvar inc t =
    7.26 -    if (inc > 0) then
    7.27 +    if inc > 0 then
    7.28        let
    7.29          val tv = typ_tvars t
    7.30          val t' = Logic.incr_tvar inc t
    7.31 -        fun update_subst (((n,i), _), s) =
    7.32 -            Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
    7.33 +        fun update_subst ((n, i), _) =
    7.34 +          Vartab.curried_update ((n, i), ([], TVar ((n, i + inc), [])));
    7.35        in
    7.36 -        (t',List.foldl update_subst Vartab.empty tv)
    7.37 +        (t', fold update_subst tv Vartab.empty)
    7.38        end
    7.39      else
    7.40        (t, Vartab.empty)
    7.41 @@ -157,9 +157,9 @@
    7.42              ((tab,max), []) ts
    7.43  
    7.44        fun idx (tab,max) (TVar ((a,i),_)) =
    7.45 -          (case Inttab.lookup (tab, i) of
    7.46 +          (case Inttab.curried_lookup tab i of
    7.47               SOME j => ((tab, max), TVar ((a,j),[]))
    7.48 -           | NONE => ((Inttab.update ((i, max), tab), max+1), TVar ((a,max),[])))
    7.49 +           | NONE => ((Inttab.curried_update (i, max) tab, max + 1), TVar ((a,max),[])))
    7.50          | idx (tab,max) (Type (t, ts)) =
    7.51            let
    7.52              val ((tab, max), ts) = idxlist idx I fst (tab, max) ts
    7.53 @@ -207,10 +207,10 @@
    7.54  
    7.55  fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) =
    7.56      (cost, axmap, (Declare cty)::actions,
    7.57 -     Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph))
    7.58 +     Symtab.curried_update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph)
    7.59      handle Symtab.DUP _ =>
    7.60             let
    7.61 -             val (Node (gty, _, _, _, _)) = the (Symtab.lookup(graph, name))
    7.62 +             val (Node (gty, _, _, _, _)) = the (Symtab.curried_lookup graph name)
    7.63             in
    7.64               if is_instance_r ty gty andalso is_instance_r gty ty then
    7.65                 g
    7.66 @@ -227,13 +227,13 @@
    7.67        val _ = axcounter := c+1
    7.68        val axname' = axname^"_"^(IntInf.toString c)
    7.69      in
    7.70 -      (Symtab.update ((axname', axname), axmap), axname')
    7.71 +      (Symtab.curried_update (axname', axname) axmap, axname')
    7.72      end
    7.73  
    7.74  fun translate_ex axmap x =
    7.75      let
    7.76        fun translate (ty, nodename, axname) =
    7.77 -          (ty, nodename, the (Symtab.lookup (axmap, axname)))
    7.78 +          (ty, nodename, the (Symtab.curried_lookup axmap axname))
    7.79      in
    7.80        case x of
    7.81          INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain))
    7.82 @@ -243,7 +243,7 @@
    7.83  
    7.84  fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body =
    7.85      let
    7.86 -      val mainnode  = (case Symtab.lookup (graph, mainref) of
    7.87 +      val mainnode  = (case Symtab.curried_lookup graph mainref of
    7.88                           NONE => def_err ("constant "^mainref^" is not declared")
    7.89                         | SOME n => n)
    7.90        val (Node (gty, defs, backs, finals, _)) = mainnode
    7.91 @@ -273,17 +273,16 @@
    7.92               let
    7.93                 val links = map normalize_edge_idx links
    7.94               in
    7.95 -               Symtab.update ((nodename,
    7.96 -                               case Symtab.lookup (edges, nodename) of
    7.97 +               Symtab.curried_update (nodename,
    7.98 +                               case Symtab.curried_lookup edges nodename of
    7.99                                   NONE => links
   7.100 -                               | SOME links' => merge_edges links' links),
   7.101 -                              edges)
   7.102 +                               | SOME links' => merge_edges links' links) edges
   7.103               end)
   7.104  
   7.105        fun make_edges ((bodyn, bodyty), edges) =
   7.106            let
   7.107              val bnode =
   7.108 -                (case Symtab.lookup (graph, bodyn) of
   7.109 +                (case Symtab.curried_lookup graph bodyn of
   7.110                     NONE => def_err "body of constant definition references undeclared constant"
   7.111                   | SOME x => x)
   7.112              val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode
   7.113 @@ -346,13 +345,13 @@
   7.114                          sys_error ("install_backrefs: closed node cannot be updated")
   7.115                        else ()
   7.116                val defnames =
   7.117 -                  (case Symtab.lookup (backs, mainref) of
   7.118 +                  (case Symtab.curried_lookup backs mainref of
   7.119                       NONE => Symtab.empty
   7.120                     | SOME s => s)
   7.121 -              val defnames' = Symtab.update_new ((axname, ()), defnames)
   7.122 -              val backs' = Symtab.update ((mainref,defnames'), backs)
   7.123 +              val defnames' = Symtab.curried_update_new (axname, ()) defnames
   7.124 +              val backs' = Symtab.curried_update (mainref, defnames') backs
   7.125              in
   7.126 -              Symtab.update ((noderef, Node (ty, defs, backs', finals, closed)), graph)
   7.127 +              Symtab.curried_update (noderef, Node (ty, defs, backs', finals, closed)) graph
   7.128              end
   7.129            else
   7.130              graph
   7.131 @@ -365,8 +364,8 @@
   7.132            else if closed = Open andalso is_instance_r gty ty then Closed else closed
   7.133  
   7.134        val thisDefnode = Defnode (ty, edges)
   7.135 -      val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new
   7.136 -        ((axname, thisDefnode), defs), backs, finals, closed)), graph)
   7.137 +      val graph = Symtab.curried_update (mainref, Node (gty, Symtab.curried_update_new
   7.138 +        (axname, thisDefnode) defs, backs, finals, closed)) graph
   7.139  
   7.140        (* Now we have to check all backreferences to this node and inform them about
   7.141           the new defnode. In this section we also check for circularity. *)
   7.142 @@ -378,8 +377,8 @@
   7.143                        getnode graph noderef
   7.144                    val _ = if closed = Final then sys_error "update_defs: closed node" else ()
   7.145                    val (Defnode (def_ty, defnode_edges)) =
   7.146 -                      the (Symtab.lookup (nodedefs, defname))
   7.147 -                  val edges = the (Symtab.lookup (defnode_edges, mainref))
   7.148 +                      the (Symtab.curried_lookup nodedefs defname)
   7.149 +                  val edges = the (Symtab.curried_lookup defnode_edges mainref)
   7.150                    val refclosed = ref false
   7.151  
   7.152                    (* the type of thisDefnode is ty *)
   7.153 @@ -417,7 +416,7 @@
   7.154                    val defnames' = if edges' = [] then
   7.155                                      defnames
   7.156                                    else
   7.157 -                                    Symtab.update ((defname, ()), defnames)
   7.158 +                                    Symtab.curried_update (defname, ()) defnames
   7.159                  in
   7.160                    if changed then
   7.161                      let
   7.162 @@ -425,16 +424,15 @@
   7.163                            if edges' = [] then
   7.164                              Symtab.delete mainref defnode_edges
   7.165                            else
   7.166 -                            Symtab.update ((mainref, edges'), defnode_edges)
   7.167 +                            Symtab.curried_update (mainref, edges') defnode_edges
   7.168                        val defnode' = Defnode (def_ty, defnode_edges')
   7.169 -                      val nodedefs' = Symtab.update ((defname, defnode'), nodedefs)
   7.170 +                      val nodedefs' = Symtab.curried_update (defname, defnode') nodedefs
   7.171                        val closed = if closed = Closed andalso Symtab.is_empty defnode_edges'
   7.172                                        andalso no_forwards nodedefs'
   7.173                                     then Final else closed
   7.174                        val graph' =
   7.175 -                          Symtab.update
   7.176 -                            ((noderef,
   7.177 -                              Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph)
   7.178 +                        Symtab.curried_update
   7.179 +                          (noderef, Node (nodety, nodedefs', nodebacks, nodefinals, closed)) graph
   7.180                      in
   7.181                        (defnames', graph')
   7.182                      end
   7.183 @@ -449,7 +447,7 @@
   7.184                (backs, graph')
   7.185              else
   7.186                let
   7.187 -                val backs' = Symtab.update_new ((noderef, defnames'), backs)
   7.188 +                val backs' = Symtab.curried_update_new (noderef, defnames') backs
   7.189                in
   7.190                  (backs', graph')
   7.191                end
   7.192 @@ -460,7 +458,7 @@
   7.193        (* If a Circular exception is thrown then we never reach this point. *)
   7.194        val (Node (gty, defs, _, finals, closed)) = getnode graph mainref
   7.195        val closed = if closed = Closed andalso no_forwards defs then Final else closed
   7.196 -      val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph)
   7.197 +      val graph = Symtab.curried_update (mainref, Node (gty, defs, backs, finals, closed)) graph
   7.198        val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions
   7.199      in
   7.200        (cost+3, axmap, actions', graph)
   7.201 @@ -484,7 +482,7 @@
   7.202      end
   7.203  
   7.204  fun finalize' (cost, axmap, history, graph) (noderef, ty) =
   7.205 -    case Symtab.lookup (graph, noderef) of
   7.206 +    case Symtab.curried_lookup graph noderef of
   7.207        NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
   7.208      | SOME (Node (nodety, defs, backs, finals, closed)) =>
   7.209        let
   7.210 @@ -521,8 +519,7 @@
   7.211              val closed = if closed = Open andalso is_instance_r nodety ty then
   7.212                             Closed else
   7.213                           closed
   7.214 -            val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals, closed)),
   7.215 -                                       graph)
   7.216 +            val graph = Symtab.curried_update (noderef, Node (nodety, defs, backs, finals, closed)) graph
   7.217  
   7.218              fun update_backref ((graph, backs), (backrefname, backdefnames)) =
   7.219                  let
   7.220 @@ -535,7 +532,7 @@
   7.221                              the (get_defnode backnode backdefname)
   7.222  
   7.223                          val (defnames', all_edges') =
   7.224 -                            case Symtab.lookup (all_edges, noderef) of
   7.225 +                            case Symtab.curried_lookup all_edges noderef of
   7.226                                NONE => sys_error "finalize: corrupt backref"
   7.227                              | SOME edges =>
   7.228                                let
   7.229 @@ -545,11 +542,11 @@
   7.230                                  if edges' = [] then
   7.231                                    (defnames, Symtab.delete noderef all_edges)
   7.232                                  else
   7.233 -                                  (Symtab.update ((backdefname, ()), defnames),
   7.234 -                                   Symtab.update ((noderef, edges'), all_edges))
   7.235 +                                  (Symtab.curried_update (backdefname, ()) defnames,
   7.236 +                                   Symtab.curried_update (noderef, edges') all_edges)
   7.237                                end
   7.238                          val defnode' = Defnode (def_ty, all_edges')
   7.239 -                        val backdefs' = Symtab.update ((backdefname, defnode'), backdefs)
   7.240 +                        val backdefs' = Symtab.curried_update (backdefname, defnode') backdefs
   7.241                          val backclosed' = if backclosed = Closed andalso
   7.242                                               Symtab.is_empty all_edges'
   7.243                                               andalso no_forwards backdefs'
   7.244 @@ -557,20 +554,20 @@
   7.245                          val backnode' =
   7.246                              Node (backty, backdefs', backbacks, backfinals, backclosed')
   7.247                        in
   7.248 -                        (Symtab.update ((backrefname, backnode'), graph), defnames')
   7.249 +                        (Symtab.curried_update (backrefname, backnode') graph, defnames')
   7.250                        end
   7.251  
   7.252                    val (graph', defnames') =
   7.253                        Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   7.254                  in
   7.255                    (graph', if Symtab.is_empty defnames' then backs
   7.256 -                           else Symtab.update ((backrefname, defnames'), backs))
   7.257 +                           else Symtab.curried_update (backrefname, defnames') backs)
   7.258                  end
   7.259              val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   7.260              val Node ( _, defs, _, _, closed) = getnode graph' noderef
   7.261              val closed = if closed = Closed andalso no_forwards defs then Final else closed
   7.262 -            val graph' = Symtab.update ((noderef, Node (nodety, defs, backs',
   7.263 -                                                        finals, closed)), graph')
   7.264 +            val graph' = Symtab.curried_update (noderef, Node (nodety, defs, backs',
   7.265 +                                                        finals, closed)) graph'
   7.266              val history' = (Finalize (noderef, ty)) :: history
   7.267            in
   7.268              (cost+1, axmap, history', graph')
   7.269 @@ -580,14 +577,14 @@
   7.270  fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty)
   7.271  
   7.272  fun update_axname ax orig_ax (cost, axmap, history, graph) =
   7.273 -  (cost, Symtab.update ((ax, orig_ax), axmap), history, graph)
   7.274 +  (cost, Symtab.curried_update (ax, orig_ax) axmap, history, graph)
   7.275  
   7.276  fun merge' (Declare cty, g) = declare' g cty
   7.277    | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) =
   7.278 -    (case Symtab.lookup (graph, name) of
   7.279 +    (case Symtab.curried_lookup graph name of
   7.280         NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
   7.281       | SOME (Node (_, defs, _, _, _)) =>
   7.282 -       (case Symtab.lookup (defs, axname) of
   7.283 +       (case Symtab.curried_lookup defs axname of
   7.284            NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
   7.285          | SOME _ => g))
   7.286    | merge' (Finalize finals, g) = finalize' g finals
   7.287 @@ -601,14 +598,14 @@
   7.288  fun finals (_, _, history, graph) =
   7.289      Symtab.foldl
   7.290        (fn (finals, (name, Node(_, _, _, ftys, _))) =>
   7.291 -          Symtab.update_new ((name, ftys), finals))
   7.292 +          Symtab.curried_update_new (name, ftys) finals)
   7.293        (Symtab.empty, graph)
   7.294  
   7.295  fun overloading_info (_, axmap, _, graph) c =
   7.296      let
   7.297 -      fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty)
   7.298 +      fun translate (ax, Defnode (ty, _)) = (the (Symtab.curried_lookup axmap ax), ty)
   7.299      in
   7.300 -      case Symtab.lookup (graph, c) of
   7.301 +      case Symtab.curried_lookup graph c of
   7.302          NONE => NONE
   7.303        | SOME (Node (ty, defnodes, _, _, state)) =>
   7.304          SOME (ty, map translate (Symtab.dest defnodes), state)
   7.305 @@ -621,7 +618,7 @@
   7.306    | monomorphicT _ = false
   7.307  
   7.308  fun monomorphic (_, _, _, graph) c =
   7.309 -  (case Symtab.lookup (graph, c) of
   7.310 +  (case Symtab.curried_lookup graph c of
   7.311      NONE => true
   7.312    | SOME (Node (ty, defnodes, _, _, _)) =>
   7.313        Symtab.min_key defnodes = Symtab.max_key defnodes andalso
     8.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Sep 01 18:48:54 2005 +0200
     8.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Sep 01 22:15:10 2005 +0200
     8.3 @@ -70,7 +70,7 @@
     8.4  struct
     8.5  
     8.6  fun datatype_info thy name =
     8.7 -  (case Symtab.lookup (DatatypesData.get thy, name) of
     8.8 +  (case Symtab.curried_lookup (DatatypesData.get thy) name of
     8.9      SOME info => info
    8.10    | NONE => error ("Unknown datatype " ^ quote name));
    8.11  
    8.12 @@ -163,14 +163,12 @@
    8.13      val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
    8.14  
    8.15    in
    8.16 -      thy |> Theory.add_path (Sign.base_name big_rec_name)
    8.17 -          |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
    8.18 -          |> DatatypesData.put
    8.19 -              (Symtab.update
    8.20 -               ((big_rec_name, dt_info), DatatypesData.get thy))
    8.21 -          |> ConstructorsData.put
    8.22 -               (foldr Symtab.update (ConstructorsData.get thy) con_pairs)
    8.23 -          |> Theory.parent_path
    8.24 +    thy
    8.25 +    |> Theory.add_path (Sign.base_name big_rec_name)
    8.26 +    |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
    8.27 +    |> DatatypesData.put (Symtab.curried_update (big_rec_name, dt_info) (DatatypesData.get thy))
    8.28 +    |> ConstructorsData.put (fold_rev Symtab.curried_update con_pairs (ConstructorsData.get thy))
    8.29 +    |> Theory.parent_path
    8.30    end;
    8.31  
    8.32  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =