--- 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 *)