# HG changeset patch
# User wenzelm
# Date 1681844604 -7200
# Node ID 04f0b689981c387129c16e2945dea4d8274f2d3d
# Parent  1d3b3bf5ea3f7f1cd97d233c9d96303737b45a9e
discontinued somewhat pointless operation: Conjunction.intr_balanced / Conjunction.elim_balanced with single hyp performs better (e.g. see AFP/351b7b576892);

diff -r 1d3b3bf5ea3f -r 04f0b689981c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Apr 18 20:54:25 2023 +0200
+++ b/src/Pure/thm.ML	Tue Apr 18 21:03:24 2023 +0200
@@ -96,8 +96,6 @@
   val transfer'': Context.generic -> thm -> thm
   val join_transfer: theory -> thm -> thm
   val join_transfer_context: Proof.context * thm -> Proof.context * thm
-  val shared_context: theory -> thm list -> thm list
-  val shared_context': Proof.context -> thm list -> thm list
   val renamed_prop: term -> thm -> thm
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
@@ -643,31 +641,6 @@
   else (Context.raw_transfer (theory_of_thm th) ctxt, th);
 
 
-(* shared context: speed-up low-level inferences *)
-
-fun shared_context thy thms0 =
-  let
-    val thms = map (transfer thy) thms0;
-    val maxidx' = fold (Integer.max o maxidx_of) thms ~1;
-    val constraints' = unions_constraints (map constraints_of thms);
-    val shyps' = Sorts.unions (map shyps_of thms);
-    val hyps' = unions_hyps (map hyps_of thms);
-  in
-    thms |> map (fn Thm (deriv, {cert, tags, tpairs, prop, ...}) =>
-      Thm (deriv,
-       {cert = cert,
-        tags = tags,
-        maxidx = maxidx',
-        constraints = constraints',
-        shyps = shyps',
-        hyps = hyps',
-        tpairs = tpairs,
-        prop = prop}))
-  end;
-
-val shared_context' = shared_context o Proof_Context.theory_of;
-
-
 (* matching *)
 
 local