--- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon Mar 27 21:48:47 2023 +0200
@@ -42,7 +42,7 @@
val get_quotients : Proof.context -> quotient Symtab.table
val get_relator_distr_data : Proof.context -> relator_distr_data Symtab.table
val get_restore_data : Proof.context -> restore_data Symtab.table
- val get_no_code_types : Proof.context -> unit Symtab.table
+ val get_no_code_types : Proof.context -> Symset.T
end
structure Lifting_Info: LIFTING_INFO =
@@ -82,7 +82,7 @@
reflexivity_rules : thm Item_Net.T,
relator_distr_data : relator_distr_data Symtab.table,
restore_data : restore_data Symtab.table,
- no_code_types : unit Symtab.table
+ no_code_types : Symset.T
}
val empty =
{ quot_maps = Symtab.empty,
@@ -90,7 +90,7 @@
reflexivity_rules = Thm.item_net,
relator_distr_data = Symtab.empty,
restore_data = Symtab.empty,
- no_code_types = Symtab.empty
+ no_code_types = Symset.empty
}
fun merge
( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1,
@@ -102,7 +102,7 @@
reflexivity_rules = Item_Net.merge (rr1, rr2),
relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),
restore_data = Symtab.join join_restore_data (rd1, rd2),
- no_code_types = Symtab.merge (K true) (nct1, nct2)
+ no_code_types = Symset.merge (nct1, nct2)
}
)
@@ -543,9 +543,9 @@
(* no_code types *)
fun add_no_code_type type_name context =
- Data.map (map_no_code_types (Symtab.update (type_name, ()))) context;
+ Data.map (map_no_code_types (Symset.insert type_name)) context;
-fun is_no_code_type context type_name = (Symtab.defined o get_no_code_types) context type_name
+fun is_no_code_type context type_name = (Symset.member o get_no_code_types) context type_name
(* setup fixed eq_onp rules *)
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Mon Mar 27 21:48:47 2023 +0200
@@ -48,15 +48,15 @@
(case String.tokens (fn c => c = #".") name of
[name] => (("", name, args), labels)
| [label, name] =>
- (if Symtab.defined labels label then
+ (if Symset.member labels label then
error ("Action label '" ^ label ^ "' already defined.")
else
();
- ((label, name, args), Symtab.insert_set label labels))
+ ((label, name, args), Symset.insert label labels))
| _ => error "Cannot parse action")
in
try read_actions ()
- |> Option.map (fn xs => fst (fold_map split_name_label xs Symtab.empty))
+ |> Option.map (fn xs => fst (fold_map split_name_label xs Symset.empty))
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon Mar 27 21:48:47 2023 +0200
@@ -27,18 +27,18 @@
structure Data = Theory_Data
(
type T =
- {ignore_consts : unit Symtab.table,
- keep_functions : unit Symtab.table,
+ {ignore_consts : Symset.T,
+ keep_functions : Symset.T,
processed_specs : ((string * thm list) list) Symtab.table};
val empty =
- {ignore_consts = Symtab.empty,
- keep_functions = Symtab.empty,
+ {ignore_consts = Symset.empty,
+ keep_functions = Symset.empty,
processed_specs = Symtab.empty};
fun merge
({ignore_consts = c1, keep_functions = k1, processed_specs = s1},
{ignore_consts = c2, keep_functions = k2, processed_specs = s2}) =
- {ignore_consts = Symtab.merge (K true) (c1, c2),
- keep_functions = Symtab.merge (K true) (k1, k2),
+ {ignore_consts = Symset.merge (c1, c2),
+ keep_functions = Symset.merge (k1, k2),
processed_specs = Symtab.merge (K true) (s1, s2)}
);
@@ -48,12 +48,12 @@
fun map_data f {ignore_consts = c, keep_functions = k, processed_specs = s} = mk_data (f (c, k, s))
fun ignore_consts cs =
- Data.map (map_data (@{apply 3(1)} (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
+ Data.map (map_data (@{apply 3(1)} (fold Symset.insert cs)))
fun keep_functions cs =
- Data.map (map_data (@{apply 3(2)} (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
+ Data.map (map_data (@{apply 3(2)} (fold Symset.insert cs)))
-fun keep_function thy = Symtab.defined (#keep_functions (Data.get thy))
+fun keep_function thy = Symset.member (#keep_functions (Data.get thy))
fun processed_specs thy = Symtab.lookup (#processed_specs (Data.get thy))
@@ -274,7 +274,7 @@
|> filter_out has_code_pred_intros
|> filter_out case_consts
|> filter_out special_cases
- |> filter_out (fn (c, _) => Symtab.defined (#ignore_consts (Data.get thy)) c)
+ |> filter_out (fn (c, _) => Symset.member (#ignore_consts (Data.get thy)) c)
|> map (fn (c, _) => (c, Sign.the_const_constraint thy c))
|> map Const
(*
--- a/src/Pure/Concurrent/task_queue.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Mon Mar 27 21:48:47 2023 +0200
@@ -181,7 +181,7 @@
end;
-structure Tasks = Table(type key = task val ord = task_ord);
+structure Tasks = Set(type key = task val ord = task_ord);
structure Task_Graph = Graph(type key = task val ord = task_ord);
@@ -205,16 +205,16 @@
(* known group members *)
-type groups = unit Tasks.table Inttab.table;
+type groups = Tasks.T Inttab.table;
fun get_tasks (groups: groups) gid =
the_default Tasks.empty (Inttab.lookup groups gid);
fun add_task (gid, task) groups =
- Inttab.update (gid, Tasks.update (task, ()) (get_tasks groups gid)) groups;
+ Inttab.update (gid, Tasks.insert task (get_tasks groups gid)) groups;
fun del_task (gid, task) groups =
- let val tasks = Tasks.delete_safe task (get_tasks groups gid) in
+ let val tasks = Tasks.remove task (get_tasks groups gid) in
if Tasks.is_empty tasks then Inttab.delete_safe gid groups
else Inttab.update (gid, tasks) groups
end;
@@ -246,9 +246,9 @@
val empty = make_queue Inttab.empty Task_Graph.empty 0 0;
fun group_tasks (Queue {groups, ...}) gs =
- fold (fn g => fn tasks => Tasks.merge (op =) (tasks, get_tasks groups (group_id g)))
+ fold (fn g => fn tasks => Tasks.merge (tasks, get_tasks groups (group_id g)))
gs Tasks.empty
- |> Tasks.keys;
+ |> Tasks.dest;
fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
@@ -298,7 +298,7 @@
let
val _ = cancel_group group Exn.Interrupt;
val running =
- Tasks.fold (fn (task, _) =>
+ Tasks.fold (fn task =>
(case get_job jobs task of Running thread => insert Thread.equal thread | _ => I))
(get_tasks groups (group_id group)) [];
in running end;
@@ -405,11 +405,11 @@
fun ready_dep _ [] = NONE
| ready_dep seen (task :: tasks) =
- if Tasks.defined seen task then ready_dep seen tasks
+ if Tasks.member seen task then ready_dep seen tasks
else
let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in
(case ready_job (task, entry) of
- NONE => ready_dep (Tasks.update (task, ()) seen) (Task_Graph.Keys.dest ds @ tasks)
+ NONE => ready_dep (Tasks.insert task seen) (Task_Graph.Keys.dest ds @ tasks)
| some => some)
end;
--- a/src/Pure/General/change_table.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/General/change_table.ML Mon Mar 27 21:48:47 2023 +0200
@@ -36,6 +36,7 @@
struct
structure Table = Table(Key);
+structure Set = Set(Key);
type key = Table.key;
exception SAME = Table.SAME;
@@ -45,7 +46,7 @@
(* optional change *)
datatype change =
- No_Change | Change of {base: serial, depth: int, changes: Table.set option};
+ No_Change | Change of {base: serial, depth: int, changes: Set.T option};
fun make_change base depth changes =
Change {base = base, depth = depth, changes = changes};
@@ -55,11 +56,11 @@
| ignore_change change = change;
fun update_change key (Change {base, depth, changes = SOME ch}) =
- make_change base depth (SOME (Table.insert (K true) (key, ()) ch))
+ make_change base depth (SOME (Set.insert key ch))
| update_change _ change = change;
fun base_change true No_Change =
- make_change (serial ()) 0 (SOME Table.empty)
+ make_change (serial ()) 0 (SOME Set.empty)
| base_change true (Change {base, depth, changes}) =
make_change base (depth + 1) changes
| base_change false (Change {base, depth, changes}) =
@@ -128,7 +129,7 @@
(case (SOME (f key (maybe_swap (x, y))) handle Table.SAME => NONE) of
NONE => tab
| SOME z => Table.update (key, z) tab)));
- in make_change_table (change', Table.fold (update o #1) ch2 tab1) end)
+ in make_change_table (change', Set.fold update ch2 tab1) end)
end;
fun merge eq =
--- a/src/Pure/General/graph.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/General/graph.ML Mon Mar 27 21:48:47 2023 +0200
@@ -76,22 +76,23 @@
val eq_key = is_equal o Key.ord;
structure Table = Table(Key);
+structure Set = Set(Key);
structure Keys =
struct
-abstype T = Keys of unit Table.table
+abstype T = Keys of Set.T
with
-val empty = Keys Table.empty;
-fun is_empty (Keys tab) = Table.is_empty tab;
+val empty = Keys Set.empty;
+fun is_empty (Keys set) = Set.is_empty set;
-fun member (Keys tab) = Table.defined tab;
-fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab);
-fun remove x (Keys tab) = Keys (Table.delete_safe x tab);
+fun member (Keys set) = Set.member set;
+fun insert x (Keys set) = Keys (Set.insert x set);
+fun remove x (Keys set) = Keys (Set.remove x set);
-fun fold f (Keys tab) = Table.fold (f o #1) tab;
-fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab;
+fun fold f (Keys set) = Set.fold f set;
+fun fold_rev f (Keys set) = Set.fold_rev f set;
fun dest keys = fold_rev cons keys [];
--- a/src/Pure/General/symbol.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/General/symbol.ML Mon Mar 27 21:48:47 2023 +0200
@@ -246,7 +246,7 @@
local
val letter_symbols =
- Symtab.make_set [
+ Symset.make [
"\<A>",
"\<B>",
"\<C>",
@@ -388,7 +388,7 @@
];
in
-val is_letter_symbol = Symtab.defined letter_symbols;
+val is_letter_symbol = Symset.member letter_symbols;
end;
--- a/src/Pure/Isar/experiment.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/Isar/experiment.ML Mon Mar 27 21:48:47 2023 +0200
@@ -16,12 +16,12 @@
structure Data = Theory_Data
(
- type T = Symtab.set;
- val empty = Symtab.empty;
- val merge = Symtab.merge (K true);
+ type T = Symset.T;
+ val empty = Symset.empty;
+ val merge = Symset.merge;
);
-fun is_experiment thy name = Symtab.defined (Data.get thy) name;
+fun is_experiment thy name = Symset.member (Data.get thy) name;
fun gen_experiment add_locale elems thy =
let
@@ -29,7 +29,7 @@
val lthy =
thy
|> add_locale experiment_name Binding.empty [] ([], []) elems
- |-> (Local_Theory.background_theory o Data.map o Symtab.insert_set);
+ |-> (Local_Theory.background_theory o Data.map o Symset.insert);
val (scope, naming) =
Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
val naming' = naming |> Name_Space.private_scope scope;
--- a/src/Pure/Isar/keyword.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/Isar/keyword.ML Mon Mar 27 21:48:47 2023 +0200
@@ -242,11 +242,11 @@
fun command_category ks =
let
- val tab = Symtab.make_set ks;
+ val set = Symset.make ks;
fun pred keywords name =
(case lookup_command keywords name of
NONE => false
- | SOME {kind, ...} => Symtab.defined tab kind);
+ | SOME {kind, ...} => Symset.member set kind);
in pred end;
val is_vacuous = command_category [diag, document_heading, document_body, document_raw];
--- a/src/Pure/Isar/proof_context.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Mar 27 21:48:47 2023 +0200
@@ -1285,17 +1285,17 @@
val serial_of = #serial oo (Name_Space.the_entry o Name_Space.space_of_table);
val ignored =
(case prev_ctxt of
- NONE => Inttab.empty
+ NONE => Intset.empty
| SOME ctxt0 =>
let val cases0 = cases_of ctxt0 in
- Inttab.build (cases0 |> Name_Space.fold_table (fn (a, _) =>
- Inttab.insert_set (serial_of cases0 a)))
+ Intset.build (cases0 |> Name_Space.fold_table (fn (a, _) =>
+ Intset.insert (serial_of cases0 a)))
end);
val cases = cases_of ctxt;
in
Name_Space.fold_table (fn (a, c) =>
let val i = serial_of cases a
- in not (Inttab.defined ignored i) ? cons (i, (a, c)) end) cases []
+ in not (Intset.member ignored i) ? cons (i, (a, c)) end) cases []
|> sort (int_ord o apply2 #1) |> map #2
end;
--- a/src/Pure/PIDE/document.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/PIDE/document.ML Mon Mar 27 21:48:47 2023 +0200
@@ -54,7 +54,7 @@
type perspective =
{required: bool, (*required node*)
- visible: Inttab.set, (*visible commands*)
+ visible: Intset.T, (*visible commands*)
visible_last: Document_ID.command option, (*last visible command*)
overlays: (string * string list) list Inttab.table}; (*command id -> print functions with args*)
@@ -79,7 +79,7 @@
fun make_perspective (required, command_ids, overlays) : perspective =
{required = required,
- visible = Inttab.make_set command_ids,
+ visible = Intset.make command_ids,
visible_last = try List.last command_ids,
overlays = Inttab.make_list overlays};
@@ -93,7 +93,7 @@
fun is_empty_perspective ({required, visible, visible_last, overlays}: perspective) =
not required andalso
- Inttab.is_empty visible andalso
+ Intset.is_empty visible andalso
is_none visible_last andalso
Inttab.is_empty overlays;
@@ -147,7 +147,7 @@
val required_node = #required o get_perspective;
val command_overlays = Inttab.lookup_list o #overlays o get_perspective;
-val command_visible = Inttab.defined o #visible o get_perspective;
+val command_visible = Intset.member o #visible o get_perspective;
val visible_last = #visible_last o get_perspective;
val visible_node = is_some o visible_last
@@ -516,14 +516,14 @@
fun all_preds P =
String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes []
|> String_Graph.all_preds nodes
- |> Symtab.make_set;
+ |> Symset.make;
val all_visible = all_preds visible_node;
val all_required = all_preds required_node;
in
- Symtab.fold (fn (a, ()) =>
- exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
- Symtab.update (a, ())) all_visible all_required
+ Symset.fold (fn a =>
+ exists (Symset.member all_visible) (String_Graph.immediate_succs nodes a) ?
+ Symset.insert a) all_visible all_required
end;
fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
@@ -548,7 +548,7 @@
val _ =
nodes |> String_Graph.schedule
(fn deps => fn (name, node) =>
- if Symtab.defined required name orelse visible_node node orelse pending_result node then
+ if Symset.member required name orelse visible_node node orelse pending_result node then
let
val future =
(singleton o Future.forks)
@@ -812,11 +812,11 @@
timeit "Document.edit_nodes"
(fn () => old_version |> fold edit_nodes edits |> edit_keywords edits);
- val consolidate = Symtab.defined (Symtab.make_set consolidate);
+ val consolidate = Symset.member (Symset.make consolidate);
val nodes = nodes_of new_version;
val required = make_required nodes;
val required0 = make_required (nodes_of old_version);
- val edited = Symtab.build (edits |> fold (Symtab.insert_set o #1));
+ val edited = Symset.build (edits |> fold (Symset.insert o #1));
val updated = timeit "Document.update" (fn () =>
nodes |> String_Graph.schedule
@@ -834,11 +834,11 @@
val maybe_consolidate = consolidate name andalso could_consolidate node;
val imports = map (apsnd Future.join) deps;
val imports_result_changed = exists (#4 o #1 o #2) imports;
- val node_required = Symtab.defined required name;
+ val node_required = Symset.member required name;
in
- if Symtab.defined edited name orelse maybe_consolidate orelse
+ if Symset.member edited name orelse maybe_consolidate orelse
visible_node node orelse imports_result_changed orelse
- Symtab.defined required0 name <> node_required
+ Symset.member required0 name <> node_required
then
let
val node0 = node_of old_version name;
@@ -906,7 +906,7 @@
val state' = state
|> define_version new_version_id new_version assigned_nodes;
- in (Symtab.keys edited, removed, assign_result, state') end);
+ in (Symset.dest edited, removed, assign_result, state') end);
end;
--- a/src/Pure/PIDE/resources.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/PIDE/resources.ML Mon Mar 27 21:48:47 2023 +0200
@@ -107,7 +107,7 @@
load_commands = []: (string * Position.T) list,
scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table},
{global_theories = Symtab.empty: string Symtab.table,
- loaded_theories = Symtab.empty: unit Symtab.table});
+ loaded_theories = Symset.empty: Symset.T});
val global_session_base =
Synchronized.var "Sessions.base" empty_session_base;
@@ -125,7 +125,7 @@
load_commands = load_commands,
scala_functions = Symtab.make scala_functions},
{global_theories = Symtab.make global_theories,
- loaded_theories = Symtab.make_set loaded_theories}));
+ loaded_theories = Symset.make loaded_theories}));
fun init_session_yxml yxml =
let
@@ -169,7 +169,7 @@
fun get_session_base2 f = get_session_base (f o #2);
fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a;
-fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a;
+fun loaded_theory a = Symset.member (get_session_base2 #loaded_theories) a;
fun check_session ctxt arg =
Completion.check_item "session"
--- a/src/Pure/Syntax/parser.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/Syntax/parser.ML Mon Mar 27 21:48:47 2023 +0200
@@ -38,15 +38,15 @@
fun tags_insert tag (tags: tags) = Symtab.update_new tag tags;
fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
-type nts = Inttab.set;
-val nts_empty: nts = Inttab.empty;
-val nts_merge: nts * nts -> nts = Inttab.merge (K true);
-fun nts_insert nt : nts -> nts = Inttab.insert_set nt;
-fun nts_member (nts: nts) = Inttab.defined nts;
-fun nts_fold f (nts: nts) = Inttab.fold (f o #1) nts;
-fun nts_subset (nts1: nts, nts2: nts) = Inttab.forall (nts_member nts2 o #1) nts1;
-fun nts_is_empty (nts: nts) = Inttab.is_empty nts;
-fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Inttab.is_single nts;
+type nts = Intset.T;
+val nts_empty: nts = Intset.empty;
+val nts_merge: nts * nts -> nts = Intset.merge;
+fun nts_insert nt : nts -> nts = Intset.insert nt;
+fun nts_member (nts: nts) = Intset.member nts;
+fun nts_fold f (nts: nts) = Intset.fold f nts;
+fun nts_subset (nts1: nts, nts2: nts) = Intset.forall (nts_member nts2) nts1;
+fun nts_is_empty (nts: nts) = Intset.is_empty nts;
+fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Intset.is_single nts;
(* tokens *)
--- a/src/Pure/context.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/context.ML Mon Mar 27 21:48:47 2023 +0200
@@ -127,7 +127,7 @@
Theory_Id of
(*identity*)
{id: serial, (*identifier*)
- ids: Inttab.set} * (*cumulative identifiers -- symbolic body content*)
+ ids: Intset.T} * (*cumulative identifiers -- symbolic body content*)
(*history*)
{name: string, (*official theory name*)
stage: stage option} (*index and counter for anonymous updates*)
@@ -215,14 +215,12 @@
(* build ids *)
-fun insert_id id ids = Inttab.update (id, ()) ids;
-
val merge_ids =
apply2 (theory_id #> rep_theory_id #> #1) #>
(fn ({id = id1, ids = ids1, ...}, {id = id2, ids = ids2, ...}) =>
- Inttab.merge (K true) (ids1, ids2)
- |> insert_id id1
- |> insert_id id2);
+ Intset.merge (ids1, ids2)
+ |> Intset.insert id1
+ |> Intset.insert id2);
(* equality and inclusion *)
@@ -231,7 +229,7 @@
val eq_thy = op = o apply2 (#id o identity_of);
val proper_subthy_id =
- apply2 (rep_theory_id #> #1) #> (fn ({id, ...}, {ids, ...}) => Inttab.defined ids id);
+ apply2 (rep_theory_id #> #1) #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id);
val proper_subthy = proper_subthy_id o apply2 theory_id;
fun subthy_id p = eq_thy_id p orelse proper_subthy_id p;
@@ -345,7 +343,7 @@
(* primitives *)
val pre_pure_thy =
- create_thy Inttab.empty (make_history PureN) (make_ancestry [] []) Datatab.empty;
+ create_thy Intset.empty (make_history PureN) (make_ancestry [] []) Datatab.empty;
local
@@ -358,7 +356,7 @@
then make_ancestry [thy] (extend_ancestors thy (ancestors_of thy))
else ancestry;
val history' = {name = name, stage = if finish then NONE else Option.map next_stage stage};
- val ids' = insert_id id ids;
+ val ids' = Intset.insert id ids;
val data' = f data;
in create_thy ids' history' ancestry' data' end;
--- a/src/Pure/more_thm.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/more_thm.ML Mon Mar 27 21:48:47 2023 +0200
@@ -253,8 +253,8 @@
structure Hyps = Proof_Data
(
- type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T};
- fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []};
+ type T = {checked_hyps: bool, hyps: Termset.T, shyps: sort Ord_List.T};
+ fun init _ : T = {checked_hyps = true, hyps = Termset.empty, shyps = []};
);
fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} =>
@@ -267,7 +267,7 @@
fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) =>
let
val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct;
- val hyps' = Termtab.update (Thm.term_of ct, ()) hyps;
+ val hyps' = Termset.insert (Thm.term_of ct) hyps;
in (checked_hyps, hyps', shyps) end);
fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
@@ -285,7 +285,7 @@
| Context.Proof ctxt =>
(case Hyps.get ctxt of
{checked_hyps = false, ...} => K true
- | {hyps, ...} => Termtab.defined hyps));
+ | {hyps, ...} => Termset.member hyps));
fun check_hyps context th =
(case undeclared_hyps context th of
--- a/src/Pure/term_ord.ML Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/term_ord.ML Mon Mar 27 21:48:47 2023 +0200
@@ -219,6 +219,9 @@
fun term_cache f = Cache.create empty lookup update f;
end;
+structure Sortset = Set(type key = sort val ord = Term_Ord.sort_ord);
+structure Termset = Set(type key = term val ord = Term_Ord.fast_term_ord);
+
structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord);
structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord);
structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord);