--- 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);
--- 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
--- 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;
--- 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