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