--- a/src/HOL/Tools/recfun_codegen.ML Mon Feb 06 20:58:56 2006 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Mon Feb 06 20:58:57 2006 +0100
@@ -26,7 +26,7 @@
val empty = Symtab.empty;
val copy = I;
val extend = I;
- fun merge _ = Symtab.merge_multi' (Drule.eq_thm_prop o pairself fst);
+ fun merge _ = Symtab.merge_list (Drule.eq_thm_prop o pairself fst);
fun print _ _ = ();
end);
@@ -44,7 +44,7 @@
val (s, _) = const_of (prop_of thm);
in
if Pattern.pattern (lhs_of thm) then
- CodegenData.put (Symtab.update_multi (s, (thm, optmod)) tab) thy
+ CodegenData.put (Symtab.update_list (s, (thm, optmod)) tab) thy
else (warn thm; thy)
end handle TERM _ => (warn thm; thy)));
--- a/src/HOL/Tools/record_package.ML Mon Feb 06 20:58:56 2006 +0100
+++ b/src/HOL/Tools/record_package.ML Mon Feb 06 20:58:57 2006 +0100
@@ -413,7 +413,7 @@
fun varify (a, S) = TVar ((a, midx), S);
val varifyT = map_type_tfree varify;
val {records,extfields,...} = RecordsData.get thy;
- val (flds,(more,_)) = split_last (Symtab.lookup_multi extfields name);
+ val (flds,(more,_)) = split_last (Symtab.lookup_list extfields name);
val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
val (subst,_) = fold (Sign.typ_unify thy) (but_last args ~~ but_last Ts) (Vartab.empty,0);
@@ -839,7 +839,7 @@
local
fun eq (s1:string) (s2:string) = (s1 = s2);
fun has_field extfields f T =
- exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_multi extfields eN))
+ exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_list extfields eN))
(dest_recTs T);
in
(* record_simproc *)
--- a/src/Pure/Syntax/syntax.ML Mon Feb 06 20:58:56 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML Mon Feb 06 20:58:57 2006 +0100
@@ -101,10 +101,10 @@
(* print (ast) translations *)
-fun lookup_tr' tab c = map fst (Symtab.lookup_multi tab c);
-fun extend_tr'tab trfuns = fold_rev Symtab.update_multi trfuns;
-fun remove_tr'tab trfuns = fold (Symtab.remove_multi SynExt.eq_trfun) trfuns;
-fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' SynExt.eq_trfun (tab1, tab2);
+fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
+fun extend_tr'tab trfuns = fold_rev Symtab.update_list trfuns;
+fun remove_tr'tab trfuns = fold (Symtab.remove_list SynExt.eq_trfun) trfuns;
+fun merge_tr'tabs tab1 tab2 = Symtab.merge_list SynExt.eq_trfun (tab1, tab2);
@@ -154,9 +154,9 @@
(* empty, extend, merge ruletabs *)
-val extend_ruletab = fold_rev (fn r => Symtab.update_multi (Ast.head_of_rule r, r));
-val remove_ruletab = fold (fn r => Symtab.remove_multi (op =) (Ast.head_of_rule r, r));
-fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
+val extend_ruletab = fold_rev (fn r => Symtab.update_list (Ast.head_of_rule r, r));
+val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r));
+fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2);
@@ -403,7 +403,7 @@
val asts = read_asts context is_logtype syn false (SynExt.typ_to_nonterm ty) str;
in
SynTrans.asts_to_terms context (lookup_tr parse_trtab)
- (map (Ast.normalize_ast (Symtab.lookup_multi parse_ruletab)) asts)
+ (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
end;
@@ -487,7 +487,7 @@
in
prt_t context curried prtabs (lookup_tr' print_ast_trtab)
(lookup_tokentr tokentrtab (! print_mode))
- (Ast.normalize_ast (Symtab.lookup_multi print_ruletab) ast)
+ (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast)
end;
val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast;
--- a/src/Pure/Thy/thm_database.ML Mon Feb 06 20:58:56 2006 +0100
+++ b/src/Pure/Thy/thm_database.ML Mon Feb 06 20:58:57 2006 +0100
@@ -105,7 +105,7 @@
"val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname;
in
Symtab.keys thms |> List.mapPartial prune
- |> Symtab.make_multi |> Symtab.dest |> sort_wrt #1
+ |> Symtab.make_list |> Symtab.dest |> sort_wrt #1
|> map (fn (prfx, entries) =>
entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx)
|> cat_lines
--- a/src/Pure/context.ML Mon Feb 06 20:58:56 2006 +0100
+++ b/src/Pure/context.ML Mon Feb 06 20:58:57 2006 +0100
@@ -416,7 +416,7 @@
fun dest_data name_of tab =
map name_of (Inttab.keys tab)
- |> map (rpair ()) |> Symtab.make_multi |> Symtab.dest
+ |> map (rpair ()) |> Symtab.make_list |> Symtab.dest
|> map (apsnd length)
|> map (fn (name, 1) => name | (name, n) => name ^ enclose "[" "]" (string_of_int n));
--- a/src/Pure/fact_index.ML Mon Feb 06 20:58:56 2006 +0100
+++ b/src/Pure/fact_index.ML Mon Feb 06 20:58:57 2006 +0100
@@ -64,8 +64,8 @@
val (cs, xs) = fold (index_thm known) ths ([], []);
val facts' = fact :: facts;
- val consts' = consts |> fold (fn c => Symtab.update_multi (c, entry)) cs;
- val frees' = frees |> fold (fn x => Symtab.update_multi (x, entry)) xs;
+ val consts' = consts |> fold (fn c => Symtab.update_list (c, entry)) cs;
+ val frees' = frees |> fold (fn x => Symtab.update_list (x, entry)) xs;
val props' = props |> K do_props ?
fold (fn th => Net.insert_term (K false) (Thm.prop_of th, th)) ths;
in Index {facts = facts', consts = consts', frees = frees', props = props'} end;
@@ -89,8 +89,8 @@
fun find idx ([], []) = facts idx
| find (Index {consts, frees, ...}) (cs, xs) =
- (map (Symtab.lookup_multi consts) cs @
- map (Symtab.lookup_multi frees) xs) |> intersects |> map #2;
+ (map (Symtab.lookup_list consts) cs @
+ map (Symtab.lookup_list frees) xs) |> intersects |> map #2;
end
--- a/src/Pure/sorts.ML Mon Feb 06 20:58:56 2006 +0100
+++ b/src/Pure/sorts.ML Mon Feb 06 20:58:57 2006 +0100
@@ -180,7 +180,7 @@
fun mg_domain (classes, arities) a S =
let
fun dom c =
- (case AList.lookup (op =) (Symtab.lookup_multi arities a) c of
+ (case AList.lookup (op =) (Symtab.lookup_list arities a) c of
NONE => raise DOMAIN (a, c)
| SOME Ss => Ss);
fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss);
@@ -241,7 +241,7 @@
else
let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in
if forall is_some ws then
- let val w = (Type (t, map (#1 o valOf) ws), S)
+ let val w = (Type (t, map (#1 o the) ws), S)
in ((w :: solved', failed'), SOME w) end
else witn_types path ts ((solved', failed'), S)
end