# 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