clarified modules;
authorwenzelm
Wed, 24 Jul 2019 11:32:18 +0200
changeset 70404 9dc99e3153b3
parent 70403 468cfd56ee03
child 70405 64fdd75c1dea
clarified modules;
src/Pure/more_thm.ML
src/Pure/thm.ML
--- 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 **)