# HG changeset patch
# User wenzelm
# Date 1703416632 -3600
# Node ID 4402c18902ec159be2c30971741bd479266b1438
# Parent  8aca79b3a9cb8333eebc4ef9117a486d021f211d
unused;

diff -r 8aca79b3a9cb -r 4402c18902ec src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sun Dec 24 12:06:20 2023 +0100
+++ b/src/Pure/global_theory.ML	Sun Dec 24 12:17:12 2023 +0100
@@ -24,8 +24,6 @@
   val all_thms_of: theory -> bool -> (string * thm) list
   val get_thm_name: theory -> Thm_Name.T * Position.T -> thm
   val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
-  val burrow_facts: ('a list -> 'b list) ->
-    ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   val register_proofs_lazy: string * Position.T -> thm list lazy -> theory -> thm list lazy * theory
   val register_proofs: string * Position.T -> thm list -> theory -> thm list * theory
   val name_multi: string * Position.T -> thm list -> ((string * Position.T) * thm) list
@@ -211,7 +209,6 @@
 (* fact specifications *)
 
 fun burrow_fact f = split_list #>> burrow f #> op ~~;
-fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
 
 
 (* register proofs *)