--- a/src/Pure/more_thm.ML Wed Jul 24 10:49:01 2019 +0200
+++ b/src/Pure/more_thm.ML Wed Jul 24 11:32:18 2019 +0200
@@ -79,7 +79,6 @@
val forall_intr_frees: thm -> thm
val unvarify_global: theory -> thm -> thm
val unvarify_axiom: theory -> string -> thm
- val close_derivation: thm -> thm
val rename_params_rule: string list * int -> thm -> thm
val rename_boundvars: term -> term -> thm -> thm
val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory
@@ -498,12 +497,6 @@
fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy;
-(* close_derivation *)
-
-fun close_derivation thm =
- if Thm.derivation_closed thm then thm else Thm.name_derivation "" thm;
-
-
(* user renaming of parameters in a subgoal *)
(*The names, if distinct, are used for the innermost parameters of subgoal i;