# HG changeset patch
# User wenzelm
# Date 1194786008 -3600
# Node ID 3e58c7cb5a73bf8d1085db2bbbb1b997ab1455a2
# Parent  5cd1302518250da7d97dec82a7c0034bbc96ee00
renamed Symtab.update_list to Symtab.cons_list;

diff -r 5cd130251825 -r 3e58c7cb5a73 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Sun Nov 11 14:00:05 2007 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Sun Nov 11 14:00:08 2007 +0100
@@ -37,7 +37,7 @@
 fun add_thm opt_module thm =
   if Pattern.pattern (lhs_of thm) then
     RecCodegenData.map
-      (Symtab.update_list ((fst o const_of o prop_of) thm, (thm, opt_module)))
+      (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module)))
   else tap (fn _ => warn thm)
   handle TERM _ => tap (fn _ => warn thm);
 
diff -r 5cd130251825 -r 3e58c7cb5a73 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Nov 11 14:00:05 2007 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Nov 11 14:00:08 2007 +0100
@@ -294,7 +294,7 @@
   in
     ExtractionData.put
       {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
-       realizers = fold (Symtab.update_list o prep_rlz thy) rs realizers,
+       realizers = fold (Symtab.cons_list o prep_rlz thy) rs realizers,
        defs = defs, expand = expand, prep = prep} thy
   end
 
diff -r 5cd130251825 -r 3e58c7cb5a73 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sun Nov 11 14:00:05 2007 +0100
+++ b/src/Pure/consts.ML	Sun Nov 11 14:00:08 2007 +0100
@@ -288,7 +288,7 @@
         val decls' = decls
           |> extend_decls naming (c, ((decl, SOME abbr), serial ()));
         val rev_abbrevs' = rev_abbrevs
-          |> fold (curry Symtab.update_list mode) (rev_abbrev lhs rhs);
+          |> fold (curry Symtab.cons_list mode) (rev_abbrev lhs rhs);
       in (decls', constraints, rev_abbrevs') end)
     |> pair (lhs, rhs)
   end;
@@ -297,7 +297,7 @@
   let
     val (T, rhs) = the_abbreviation consts c;
     val rev_abbrevs' = rev_abbrevs
-      |> fold (curry Symtab.update_list mode) (rev_abbrev (Const (c, T)) rhs);
+      |> fold (curry Symtab.cons_list mode) (rev_abbrev (Const (c, T)) rhs);
   in (decls, constraints, rev_abbrevs') end);
 
 end;
diff -r 5cd130251825 -r 3e58c7cb5a73 src/Pure/fact_index.ML
--- a/src/Pure/fact_index.ML	Sun Nov 11 14:00:05 2007 +0100
+++ b/src/Pure/fact_index.ML	Sun Nov 11 14:00:08 2007 +0100
@@ -67,8 +67,8 @@
     val (facts', consts', frees') =
       if do_index then
        (fact :: facts,
-        consts |> fold (fn c => Symtab.update_list (c, entry)) cs,
-        frees |> fold (fn x => Symtab.update_list (x, entry)) xs)
+        consts |> fold (fn c => Symtab.cons_list (c, entry)) cs,
+        frees |> fold (fn x => Symtab.cons_list (x, entry)) xs)
       else (facts, consts, frees);
     val props' =
       if do_props then props |> fold (fn th => Net.insert_term (K false) (Thm.prop_of th, th)) ths