# HG changeset patch
# User wenzelm
# Date 975011390 -3600
# Node ID 8430c8fa8a9fca399a2d33603791c60e29177b95
# Parent  3db037155f0efe0a0341ba2873fbfbc761e8e3a2
standard: close_derivation;

diff -r 3db037155f0e -r 8430c8fa8a9f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Nov 23 21:29:35 2000 +0100
+++ b/src/Pure/drule.ML	Thu Nov 23 21:29:50 2000 +0100
@@ -90,6 +90,7 @@
   val tag_assumption    : 'a attribute
   val tag_internal      : 'a attribute
   val has_internal	: tag list -> bool
+  val close_derivation  : thm -> thm
   val compose_single    : thm * int * thm -> thm
   val add_rules		: thm list -> thm list -> thm list
   val del_rules		: thm list -> thm list -> thm list
@@ -322,13 +323,18 @@
 
 (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
     all generality expressed by Vars having index 0.*)
+
+fun close_derivation thm =
+  if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm)
+  else thm;
+
 fun standard th =
-  let val {maxidx,...} = rep_thm th
-  in
-    th |> implies_intr_hyps
-       |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
-       |> strip_shyps_warning
-       |> zero_var_indexes |> Thm.varifyT |> Thm.compress
+  let val {maxidx,...} = rep_thm th in
+    th
+    |> implies_intr_hyps
+    |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
+    |> strip_shyps_warning
+    |> zero_var_indexes |> Thm.varifyT |> Thm.compress |> close_derivation
   end;