# HG changeset patch
# User wenzelm
# Date 1683280373 -7200
# Node ID fa3474ed80bea477184e182ff296ce7245b8cbf4
# Parent  81b953729ff70e7524d6c7d990b7a8be99dffca1
unused;

diff -r 81b953729ff7 -r fa3474ed80be src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri May 05 11:47:38 2023 +0200
+++ b/src/Pure/thm.ML	Fri May 05 11:52:53 2023 +0200
@@ -400,7 +400,6 @@
 in
 
 val union_constraints = Ord_List.union constraint_ord;
-val unions_constraints = Ord_List.unions constraint_ord;
 
 fun insert_constraints thy (T, S) =
   let
@@ -481,7 +480,6 @@
 
 
 val union_hyps = Ord_List.union Term_Ord.fast_term_ord;
-val unions_hyps = Ord_List.unions Term_Ord.fast_term_ord;
 val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord;
 val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord;
 
@@ -503,7 +501,6 @@
 
 val maxidx_of = #maxidx o rep_thm;
 fun maxidx_thm th i = Int.max (maxidx_of th, i);
-val constraints_of = #constraints o rep_thm;
 val shyps_of = #shyps o rep_thm;
 val hyps_of = #hyps o rep_thm;
 val prop_of = #prop o rep_thm;