# HG changeset patch
# User wenzelm
# Date 1208012440 -7200
# Node ID 63306cb94313378d0584f9f1b2443b4694b004ed
# Parent  dac6d56b7c8dde229d1594659a99c1344a68fbe3
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);

diff -r dac6d56b7c8d -r 63306cb94313 src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Sat Apr 12 17:00:38 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Sat Apr 12 17:00:40 2008 +0200
@@ -311,7 +311,7 @@
                                 |> fold_rev (implies_intr o cprop_of) h_assums
                                 |> fold_rev (implies_intr o cprop_of) ags
                                 |> fold_rev forall_intr cqs
-                                |> Goal.close_result
+                                |> Thm.close_derivation
     in
       replace_lemma
     end
@@ -439,7 +439,7 @@
                                   |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
 
         val goalstate =  Conjunction.intr graph_is_function complete
-                          |> Goal.close_result
+                          |> Thm.close_derivation
                           |> Goal.protect
                           |> fold_rev (implies_intr o cprop_of) compat
                           |> implies_intr (cprop_of complete)
diff -r dac6d56b7c8d -r 63306cb94313 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Apr 12 17:00:38 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Apr 12 17:00:40 2008 +0200
@@ -63,7 +63,7 @@
 fun fundef_afterqed do_print fixes post defname cont sort_cont cnames [[proof]] lthy =
     let
       val FundefResult {fs, R, psimps, trsimps,  simple_pinducts, termination, domintros, cases, ...} = 
-          cont (Goal.close_result proof)
+          cont (Thm.close_derivation proof)
 
       val fnames = map (fst o fst) fixes
       val qualify = NameSpace.qualified defname
@@ -115,7 +115,7 @@
     let
       val FundefCtxData { add_simps, case_names, psimps, pinducts, defname, ... } = data
 
-      val totality = Goal.close_result totality
+      val totality = Thm.close_derivation totality
 
       val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
 
diff -r dac6d56b7c8d -r 63306cb94313 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Apr 12 17:00:38 2008 +0200
+++ b/src/Pure/Isar/class.ML	Sat Apr 12 17:00:40 2008 +0200
@@ -314,7 +314,7 @@
     val assm_intro = proto_assm_intro
       |> Option.map instantiate_base_sort
       |> Option.map (MetaSimplifier.rewrite_rule defs)
-      |> Option.map Goal.close_result;
+      |> Option.map Thm.close_derivation;
     val class_intro = (#intro o AxClass.get_info thy) class;
     val fixate = Thm.instantiate
       (map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)),
@@ -334,7 +334,7 @@
         |> replicate num_trivs;
     val of_class = (fixate class_intro OF of_class_sups OF locale_dests OF pred_trivs)
       |> Drule.standard'
-      |> Goal.close_result;
+      |> Thm.close_derivation;
     val this_intro = assm_intro |> the_default class_intro;
   in
     thy
diff -r dac6d56b7c8d -r 63306cb94313 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Apr 12 17:00:38 2008 +0200
+++ b/src/Pure/Isar/element.ML	Sat Apr 12 17:00:40 2008 +0200
@@ -291,13 +291,13 @@
   Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
 
 fun prove_witness ctxt t tac =
-  Witness (t, Goal.close_result (Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
+  Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
     Tactic.rtac Drule.protectI 1 THEN tac)));
 
-val close_witness = map_witness (fn (t, th) => (t, Goal.close_result th));
+val close_witness = map_witness (fn (t, th) => (t, Thm.close_derivation th));
 
 fun conclude_witness (Witness (_, th)) =
-  Goal.close_result (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
+  Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
 
 fun compose_witness (Witness (_, th)) r =
   let
diff -r dac6d56b7c8d -r 63306cb94313 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Apr 12 17:00:38 2008 +0200
+++ b/src/Pure/goal.ML	Sat Apr 12 17:00:40 2008 +0200
@@ -20,7 +20,6 @@
   val conclude: thm -> thm
   val finish: thm -> thm
   val norm_result: thm -> thm
-  val close_result: thm -> thm
   val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
@@ -84,18 +83,12 @@
 
 (** results **)
 
-(* normal form *)
-
 val norm_result =
   Drule.flexflex_unique
   #> MetaSimplifier.norm_hhf_protect
   #> Thm.strip_shyps
   #> Drule.zero_var_indexes;
 
-val close_result =
-  Thm.compress
-  #> Drule.close_derivation;
-
 
 
 (** tactical theorem proving **)
diff -r dac6d56b7c8d -r 63306cb94313 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Apr 12 17:00:38 2008 +0200
+++ b/src/Pure/more_thm.ML	Sat Apr 12 17:00:40 2008 +0200
@@ -53,6 +53,7 @@
   val read_cterm: theory -> string * typ -> cterm
   val elim_implies: thm -> thm -> thm
   val unvarify: thm -> thm
+  val close_derivation: thm -> thm
   val add_axiom: term list -> bstring * term -> theory -> thm * theory
   val add_def: bool -> bool -> bstring * term -> theory -> thm * theory
 end;
@@ -250,6 +251,10 @@
       in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
   in Thm.instantiate (instT, inst) th end;
 
+fun close_derivation thm =
+  if Thm.get_name thm = "" then Thm.put_name "" thm
+  else thm;
+
 
 
 (** specification primitives **)