diff --git a/src/Pure/General/set.ML b/src/Pure/General/set.ML
new file mode 100644
--- /dev/null
+++ b/src/Pure/General/set.ML
@@ -0,0 +1,279 @@
+(*  Title:      Pure/General/set.ML
+    Author:     Makarius
+
+Efficient representation of sets (see also Pure/General/table.ML).
+*)
+
+signature SET =
+sig
+  type elem
+  type T
+  val empty: T
+  val build: (T -> T) -> T
+  val is_empty: T -> bool
+  val is_single: T -> bool
+  val fold: (elem -> 'a -> 'a) -> T -> 'a -> 'a
+  val fold_rev: (elem -> 'a -> 'a) -> T -> 'a -> 'a
+  val dest: T -> elem list
+  val exists: (elem -> bool) -> T -> bool
+  val forall: (elem -> bool) -> T -> bool
+  val member: T -> elem -> bool
+  val insert: elem -> T -> T
+  val make: elem list -> T
+  val merge: T * T -> T
+  val remove: elem -> T -> T
+end;
+
+functor Set(Key: KEY): SET =
+struct
+
+(* datatype *)
+
+type elem = Key.key;
+
+datatype T =
+  Empty |
+  Branch2 of T * elem * T |
+  Branch3 of T * elem * T * elem * T;
+
+
+(* empty and single *)
+
+val empty = Empty;
+
+fun build (f: T -> T) = f empty;
+
+fun is_empty Empty = true
+  | is_empty _ = false;
+
+fun is_single (Branch2 (Empty, _, Empty)) = true
+  | is_single _ = false;
+
+
+(* fold combinators *)
+
+fun fold_set f =
+  let
+    fun fold Empty x = x
+      | fold (Branch2 (left, e, right)) x =
+          fold right (f e (fold left x))
+      | fold (Branch3 (left, e1, mid, e2, right)) x =
+          fold right (f e2 (fold mid (f e1 (fold left x))));
+  in fold end;
+
+fun fold_rev_set f =
+  let
+    fun fold Empty x = x
+      | fold (Branch2 (left, e, right)) x =
+          fold left (f e (fold right x))
+      | fold (Branch3 (left, e1, mid, e2, right)) x =
+          fold left (f e1 (fold mid (f e2 (fold right x))));
+  in fold end;
+
+fun dest tab = fold_rev_set cons tab [];
+
+
+(* exists and forall *)
+
+fun exists pred =
+  let
+    fun ex Empty = false
+      | ex (Branch2 (left, e, right)) =
+          ex left orelse pred e orelse ex right
+      | ex (Branch3 (left, e1, mid, e2, right)) =
+          ex left orelse pred e1 orelse ex mid orelse pred e2 orelse ex right;
+  in ex end;
+
+fun forall pred = not o exists (not o pred);
+
+
+(* member *)
+
+fun member set elem =
+  let
+    fun mem Empty = false
+      | mem (Branch2 (left, e, right)) =
+          (case Key.ord (elem, e) of
+            LESS => mem left
+          | EQUAL => true
+          | GREATER => mem right)
+      | mem (Branch3 (left, e1, mid, e2, right)) =
+          (case Key.ord (elem, e1) of
+            LESS => mem left
+          | EQUAL => true
+          | GREATER =>
+              (case Key.ord (elem, e2) of
+                LESS => mem mid
+              | EQUAL => true
+              | GREATER => mem right));
+  in mem set end;
+
+
+(* insert *)
+
+datatype growth = Stay of T | Sprout of T * elem * T;
+
+fun insert elem set =
+  if member set elem then set
+  else
+    let
+      fun ins Empty = Sprout (Empty, elem, Empty)
+        | ins (Branch2 (left, e, right)) =
+            (case Key.ord (elem, e) of
+              LESS =>
+                (case ins left of
+                  Stay left' => Stay (Branch2 (left', e, right))
+                | Sprout (left1, e', left2) => Stay (Branch3 (left1, e', left2, e, right)))
+            | EQUAL => Stay (Branch2 (left, e, right))
+            | GREATER =>
+                (case ins right of
+                  Stay right' => Stay (Branch2 (left, e, right'))
+                | Sprout (right1, e', right2) =>
+                    Stay (Branch3 (left, e, right1, e', right2))))
+        | ins (Branch3 (left, e1, mid, e2, right)) =
+            (case Key.ord (elem, e1) of
+              LESS =>
+                (case ins left of
+                  Stay left' => Stay (Branch3 (left', e1, mid, e2, right))
+                | Sprout (left1, e', left2) =>
+                    Sprout (Branch2 (left1, e', left2), e1, Branch2 (mid, e2, right)))
+            | EQUAL => Stay (Branch3 (left, e1, mid, e2, right))
+            | GREATER =>
+                (case Key.ord (elem, e2) of
+                  LESS =>
+                    (case ins mid of
+                      Stay mid' => Stay (Branch3 (left, e1, mid', e2, right))
+                    | Sprout (mid1, e', mid2) =>
+                        Sprout (Branch2 (left, e1, mid1), e', Branch2 (mid2, e2, right)))
+                | EQUAL => Stay (Branch3 (left, e1, mid, e2, right))
+                | GREATER =>
+                    (case ins right of
+                      Stay right' => Stay (Branch3 (left, e1, mid, e2, right'))
+                    | Sprout (right1, e', right2) =>
+                        Sprout (Branch2 (left, e1, mid), e2, Branch2 (right1, e', right2)))));
+    in
+      (case ins set of
+        Stay set' => set'
+      | Sprout br => Branch2 br)
+    end;
+
+fun make elems = build (fold insert elems);
+
+fun merge (set1, set2) =
+  if pointer_eq (set1, set2) then set1
+  else if is_empty set1 then set2
+  else fold_set insert set2 set1;
+
+
+(* remove *)
+
+local
+
+fun compare NONE _ = LESS
+  | compare (SOME e1) e2 = Key.ord (e1, e2);
+
+fun if_eq EQUAL x y = x
+  | if_eq _ x y = y;
+
+exception UNDEF of elem;
+
+(*literal copy from table.ML -- by Stefan Berghofer*)
+fun del (SOME k) Empty = raise UNDEF k
+  | del NONE (Branch2 (Empty, p, Empty)) = (p, (true, Empty))
+  | del NONE (Branch3 (Empty, p, Empty, q, Empty)) =
+      (p, (false, Branch2 (Empty, q, Empty)))
+  | del k (Branch2 (Empty, p, Empty)) =
+      (case compare k p of
+        EQUAL => (p, (true, Empty))
+      | _ => raise UNDEF (the k))
+  | del k (Branch3 (Empty, p, Empty, q, Empty)) =
+      (case compare k p of
+        EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
+      | _ =>
+        (case compare k q of
+          EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
+        | _ => raise UNDEF (the k)))
+  | del k (Branch2 (l, p, r)) =
+      (case compare k p of
+        LESS =>
+          (case del k l of
+            (p', (false, l')) => (p', (false, Branch2 (l', p, r)))
+          | (p', (true, l')) => (p', case r of
+              Branch2 (rl, rp, rr) =>
+                (true, Branch3 (l', p, rl, rp, rr))
+            | Branch3 (rl, rp, rm, rq, rr) => (false, Branch2
+                (Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr)))))
+      | ord =>
+          (case del (if_eq ord NONE k) r of
+            (p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r')))
+          | (p', (true, r')) => (p', case l of
+              Branch2 (ll, lp, lr) =>
+                (true, Branch3 (ll, lp, lr, if_eq ord p' p, r'))
+            | Branch3 (ll, lp, lm, lq, lr) => (false, Branch2
+                (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r'))))))
+  | del k (Branch3 (l, p, m, q, r)) =
+      (case compare k q of
+        LESS =>
+          (case compare k p of
+            LESS =>
+              (case del k l of
+                (p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r)))
+              | (p', (true, l')) => (p', (false, case (m, r) of
+                  (Branch2 (ml, mp, mr), Branch2 _) =>
+                    Branch2 (Branch3 (l', p, ml, mp, mr), q, r)
+                | (Branch3 (ml, mp, mm, mq, mr), _) =>
+                    Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r)
+                | (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) =>
+                    Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp,
+                      Branch2 (rm, rq, rr)))))
+          | ord =>
+              (case del (if_eq ord NONE k) m of
+                (p', (false, m')) =>
+                  (p', (false, Branch3 (l, if_eq ord p' p, m', q, r)))
+              | (p', (true, m')) => (p', (false, case (l, r) of
+                  (Branch2 (ll, lp, lr), Branch2 _) =>
+                    Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r)
+                | (Branch3 (ll, lp, lm, lq, lr), _) =>
+                    Branch3 (Branch2 (ll, lp, lm), lq,
+                      Branch2 (lr, if_eq ord p' p, m'), q, r)
+                | (_, Branch3 (rl, rp, rm, rq, rr)) =>
+                    Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp,
+                      Branch2 (rm, rq, rr))))))
+      | ord =>
+          (case del (if_eq ord NONE k) r of
+            (q', (false, r')) =>
+              (q', (false, Branch3 (l, p, m, if_eq ord q' q, r')))
+          | (q', (true, r')) => (q', (false, case (l, m) of
+              (Branch2 _, Branch2 (ml, mp, mr)) =>
+                Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r'))
+            | (_, Branch3 (ml, mp, mm, mq, mr)) =>
+                Branch3 (l, p, Branch2 (ml, mp, mm), mq,
+                  Branch2 (mr, if_eq ord q' q, r'))
+            | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) =>
+                Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp,
+                  Branch2 (mr, if_eq ord q' q, r'))))));
+
+in
+
+fun remove elem set =
+  if member set elem then snd (snd (del (SOME elem) set)) else set;
+
+end;
+
+
+(* ML pretty-printing *)
+
+val _ =
+  ML_system_pp (fn depth => fn _ => fn set =>
+    ML_Pretty.to_polyml
+      (ML_Pretty.enum "," "{" "}" (ML_Pretty.from_polyml o ML_system_pretty) (dest set, depth)));
+
+
+(*final declarations of this structure!*)
+val fold = fold_set;
+val fold_rev = fold_rev_set;
+
+end;
+
+structure Intset = Set(type key = int val ord = int_ord);
+structure Symset = Set(type key = string val ord = fast_string_ord);
diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML
+++ b/src/Pure/ROOT.ML
@@ -1,368 +1,369 @@
 (*  Title:      Pure/ROOT.ML
     Author:     Makarius
 
 Main entry point for the Isabelle/Pure bootstrap process.
 
 Note: When this file is open in the Prover IDE, the ML files of
 Isabelle/Pure can be explored interactively. This is a separate copy of
 Pure within Pure: it does not affect the running logic session.
 *)
 
 chapter "Isabelle/Pure bootstrap";
 
 ML_file "ML/ml_name_space.ML";
 
 
 section "Bootstrap phase 0: Poly/ML setup";
 
 ML_file "ML/ml_init.ML";
 ML_file "ML/ml_system.ML";
 
 ML_file "General/basics.ML";
 ML_file "General/symbol_explode.ML";
 
 ML_file "Concurrent/multithreading.ML";
 ML_file "Concurrent/unsynchronized.ML";
 ML_file "Concurrent/synchronized.ML";
 ML_file "Concurrent/counter.ML";
 
 ML_file "ML/ml_heap.ML";
 ML_file "ML/ml_print_depth0.ML";
 ML_file "ML/ml_pretty.ML";
 ML_file "ML/ml_compiler0.ML";
 
 
 section "Bootstrap phase 1: towards ML within position context";
 
 subsection "Library of general tools";
 
 ML_file "library.ML";
 ML_file "General/print_mode.ML";
 ML_file "General/alist.ML";
 ML_file "General/table.ML";
+ML_file "General/set.ML";
 
 ML_file "General/random.ML";
 ML_file "General/value.ML";
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
 ML_file "PIDE/markup.ML";
 ML_file "General/utf8.ML";
 ML_file "General/scan.ML";
 ML_file "General/source.ML";
 ML_file "General/symbol.ML";
 ML_file "General/position.ML";
 ML_file "General/symbol_pos.ML";
 ML_file "General/input.ML";
 ML_file "General/comment.ML";
 ML_file "General/antiquote.ML";
 ML_file "ML/ml_lex.ML";
 ML_file "ML/ml_compiler1.ML";
 
 
 section "Bootstrap phase 2: towards ML within Isar context";
 
 subsection "Library of general tools";
 
 ML_file "General/integer.ML";
 ML_file "General/stack.ML";
 ML_file "General/queue.ML";
 ML_file "General/heap.ML";
 ML_file "General/same.ML";
 ML_file "General/ord_list.ML";
 ML_file "General/balanced_tree.ML";
 ML_file "General/linear_set.ML";
 ML_file "General/buffer.ML";
 ML_file "General/pretty.ML";
 ML_file "General/rat.ML";
 ML_file "PIDE/xml.ML";
 ML_file "General/path.ML";
 ML_file "General/url.ML";
 ML_file "System/bash.ML";
 ML_file "General/file_stream.ML";
 ML_file "General/bytes.ML";
 ML_file "General/file.ML";
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
 ML_file "General/seq.ML";
 ML_file "General/time.ML";
 ML_file "General/timing.ML";
 ML_file "General/sha1.ML";
 
 ML_file "PIDE/yxml.ML";
 ML_file "ML/ml_profiling.ML";
 ML_file "PIDE/byte_message.ML";
 ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document_id.ML";
 ML_file "General/socket_io.ML";
 
 ML_file "General/change_table.ML";
 ML_file "General/graph.ML";
 
 ML_file "System/options.ML";
 
 
 subsection "Fundamental structures";
 
 ML_file "name.ML";
 ML_file "term.ML";
 ML_file "context.ML";
 ML_file "config.ML";
 ML_file "context_position.ML";
 ML_file "soft_type_system.ML";
 
 
 subsection "Concurrency within the ML runtime";
 
 ML_file "ML/exn_properties.ML";
 ML_file_no_debug "ML/exn_debugger.ML";
 
 ML_file "Concurrent/thread_data_virtual.ML";
 ML_file "Concurrent/isabelle_thread.ML";
 ML_file "Concurrent/single_assignment.ML";
 
 ML_file "Concurrent/par_exn.ML";
 ML_file "Concurrent/task_queue.ML";
 ML_file "Concurrent/future.ML";
 ML_file "Concurrent/event_timer.ML";
 ML_file "Concurrent/timeout.ML";
 ML_file "Concurrent/lazy.ML";
 ML_file "Concurrent/par_list.ML";
 
 ML_file "Concurrent/mailbox.ML";
 ML_file "Concurrent/cache.ML";
 
 ML_file "PIDE/active.ML";
 ML_file "Thy/export.ML";
 
 
 subsection "Inner syntax";
 
 ML_file "Syntax/type_annotation.ML";
 ML_file "Syntax/term_position.ML";
 ML_file "Syntax/lexicon.ML";
 ML_file "Syntax/ast.ML";
 ML_file "Syntax/syntax_ext.ML";
 ML_file "Syntax/parser.ML";
 ML_file "Syntax/syntax_trans.ML";
 ML_file "Syntax/mixfix.ML";
 ML_file "Syntax/printer.ML";
 ML_file "Syntax/syntax.ML";
 
 
 subsection "Core of tactical proof system";
 
 ML_file "term_ord.ML";
 ML_file "term_items.ML";
 ML_file "term_subst.ML";
 ML_file "General/completion.ML";
 ML_file "General/name_space.ML";
 ML_file "sorts.ML";
 ML_file "type.ML";
 ML_file "logic.ML";
 ML_file "Syntax/simple_syntax.ML";
 ML_file "net.ML";
 ML_file "item_net.ML";
 ML_file "envir.ML";
 ML_file "consts.ML";
 ML_file "term_xml.ML";
 ML_file "primitive_defs.ML";
 ML_file "sign.ML";
 ML_file "defs.ML";
 ML_file "term_sharing.ML";
 ML_file "pattern.ML";
 ML_file "unify.ML";
 ML_file "theory.ML";
 ML_file "proofterm.ML";
 ML_file "thm.ML";
 ML_file "cterm_items.ML";
 ML_file "more_pattern.ML";
 ML_file "more_unify.ML";
 ML_file "more_thm.ML";
 
 ML_file "facts.ML";
 ML_file "thm_name.ML";
 ML_file "global_theory.ML";
 ML_file "pure_thy.ML";
 ML_file "drule.ML";
 ML_file "morphism.ML";
 ML_file "variable.ML";
 ML_file "conv.ML";
 ML_file "goal_display.ML";
 ML_file "tactical.ML";
 ML_file "search.ML";
 ML_file "tactic.ML";
 ML_file "raw_simplifier.ML";
 ML_file "conjunction.ML";
 ML_file "assumption.ML";
 
 
 subsection "Isar -- Intelligible Semi-Automated Reasoning";
 
 (*ML support and global execution*)
 ML_file "ML/ml_syntax.ML";
 ML_file "ML/ml_env.ML";
 ML_file "ML/ml_options.ML";
 ML_file "ML/ml_print_depth.ML";
 ML_file_no_debug "Isar/runtime.ML";
 ML_file "PIDE/execution.ML";
 ML_file "ML/ml_compiler.ML";
 
 ML_file "skip_proof.ML";
 ML_file "goal.ML";
 
 (*outer syntax*)
 ML_file "Isar/keyword.ML";
 ML_file "Isar/token.ML";
 ML_file "Isar/parse.ML";
 ML_file "Thy/document_source.ML";
 ML_file "Thy/thy_header.ML";
 ML_file "Thy/document_marker.ML";
 
 (*proof context*)
 ML_file "Isar/object_logic.ML";
 ML_file "Isar/rule_cases.ML";
 ML_file "Isar/auto_bind.ML";
 ML_file "type_infer.ML";
 ML_file "Syntax/local_syntax.ML";
 ML_file "Isar/proof_context.ML";
 ML_file "type_infer_context.ML";
 ML_file "Syntax/syntax_phases.ML";
 ML_file "Isar/args.ML";
 
 (*theory specifications*)
 ML_file "Isar/local_defs.ML";
 ML_file "Isar/local_theory.ML";
 ML_file "Isar/entity.ML";
 ML_file "PIDE/command_span.ML";
 ML_file "Thy/thy_element.ML";
 ML_file "Thy/markdown.ML";
 ML_file "Thy/latex.ML";
 
 (*ML with context and antiquotations*)
 ML_file "ML/ml_context.ML";
 ML_file "ML/ml_antiquotation.ML";
 ML_file "ML/ml_compiler2.ML";
 ML_file "ML/ml_antiquotations.ML";
 
 
 section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";
 
 (*basic proof engine*)
 ML_file "par_tactical.ML";
 ML_file "context_tactic.ML";
 ML_file "Isar/attrib.ML";
 ML_file "Isar/proof_display.ML";
 ML_file "Isar/context_rules.ML";
 ML_file "Isar/method.ML";
 ML_file "Isar/proof.ML";
 ML_file "Isar/element.ML";
 ML_file "Isar/obtain.ML";
 ML_file "Isar/subgoal.ML";
 ML_file "Isar/calculation.ML";
 
 (*local theories and targets*)
 ML_file "Isar/locale.ML";
 ML_file "Isar/generic_target.ML";
 ML_file "Isar/bundle.ML";
 ML_file "Isar/overloading.ML";
 ML_file "axclass.ML";
 ML_file "Isar/class.ML";
 ML_file "Isar/named_target.ML";
 ML_file "Isar/expression.ML";
 ML_file "Isar/interpretation.ML";
 ML_file "Isar/class_declaration.ML";
 ML_file "Isar/target_context.ML";
 ML_file "Isar/experiment.ML";
 ML_file "simplifier.ML";
 ML_file "Tools/plugin.ML";
 
 (*executable theory content*)
 ML_file "Isar/code.ML";
 
 (*specifications*)
 ML_file "Isar/spec_rules.ML";
 ML_file "Isar/specification.ML";
 ML_file "Isar/parse_spec.ML";
 ML_file "Isar/typedecl.ML";
 
 (*toplevel transactions*)
 ML_file "Isar/proof_node.ML";
 ML_file "Isar/toplevel.ML";
 
 (*proof term operations*)
 ML_file "Proof/proof_rewrite_rules.ML";
 ML_file "Proof/proof_syntax.ML";
 ML_file "Proof/proof_checker.ML";
 ML_file "Proof/extraction.ML";
 
 (*Isabelle system*)
 ML_file "PIDE/protocol_command.ML";
 ML_file "System/java.ML";
 ML_file "System/scala.ML";
 ML_file "System/process_result.ML";
 ML_file "System/isabelle_system.ML";
 
 
 (*theory documents*)
 ML_file "Thy/term_style.ML";
 ML_file "Isar/outer_syntax.ML";
 ML_file "Thy/document_antiquotation.ML";
 ML_file "Thy/document_output.ML";
 ML_file "Thy/document_antiquotations.ML";
 ML_file "General/graph_display.ML";
 ML_file "pure_syn.ML";
 ML_file "PIDE/resources.ML";
 ML_file "PIDE/command.ML";
 ML_file "PIDE/query_operation.ML";
 ML_file "Thy/thy_info.ML";
 ML_file "thm_deps.ML";
 ML_file "Thy/export_theory.ML";
 ML_file "Thy/sessions.ML";
 ML_file "PIDE/session.ML";
 ML_file "PIDE/document.ML";
 
 (*ML add-ons*)
 ML_file "ML/ml_pp.ML";
 ML_file "ML/ml_thms.ML";
 ML_file "ML/ml_instantiate.ML";
 ML_file "ML/ml_file.ML";
 ML_file "ML/ml_pid.ML";
 
 (*theory and proof operations*)
 ML_file "Isar/isar_cmd.ML";
 
 
 subsection "Isabelle/Isar system";
 
 ML_file "System/command_line.ML";
 ML_file "System/message_channel.ML";
 ML_file "System/isabelle_process.ML";
 ML_file "System/scala_compiler.ML";
 ML_file "System/isabelle_tool.ML";
 ML_file "Thy/bibtex.ML";
 ML_file "PIDE/protocol.ML";
 ML_file "General/output_primitives_virtual.ML";
 
 
 subsection "Miscellaneous tools and packages for Pure Isabelle";
 
 ML_file "General/base64.ML";
 ML_file "General/xz.ML";
 ML_file "General/zstd.ML";
 ML_file "Tools/prismjs.ML";
 ML_file "Tools/build.ML";
 ML_file "Tools/named_thms.ML";
 ML_file "Tools/print_operation.ML";
 ML_file "Tools/rail.ML";
 ML_file "Tools/rule_insts.ML";
 ML_file "Tools/thy_deps.ML";
 ML_file "Tools/class_deps.ML";
 ML_file "Tools/find_theorems.ML";
 ML_file "Tools/find_consts.ML";
 ML_file "Tools/simplifier_trace.ML";
 ML_file_no_debug "Tools/debugger.ML";
 ML_file "Tools/named_theorems.ML";
 ML_file "Tools/doc.ML";
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML";