--- 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;
--- a/src/Pure/thm.ML Wed Jul 24 10:49:01 2019 +0200
+++ b/src/Pure/thm.ML Wed Jul 24 11:32:18 2019 +0200
@@ -104,6 +104,7 @@
val derivation_closed: thm -> bool
val derivation_name: thm -> string
val name_derivation: string -> thm -> thm
+ val close_derivation: thm -> thm
val axiom: theory -> string -> thm
val axioms_of: theory -> (string * thm) list
val get_tags: thm -> Properties.T
@@ -760,6 +761,9 @@
val der' = make_deriv [] [] [pthm] proof;
in Thm (der', args) end;
+fun close_derivation thm =
+ if derivation_closed thm then thm else name_derivation "" thm;
+
(** Axioms **)