renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;

--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat May 08 17:10:27 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat May 08 16:53:53 2010 +0200
@@ -120,7 +120,7 @@
           REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
             REPEAT (etac allE i) THEN atac i)) 1)]);
 
-    val ind_name = Thm.get_name induct;
+    val ind_name = Thm.derivation_name induct;
     val vs = map (fn i => List.nth (pnames, i)) is;
     val (thm', thy') = thy
       |> Sign.root_path
@@ -191,7 +191,7 @@
             [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
              resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
 
-    val exh_name = Thm.get_name exhaust;
+    val exh_name = Thm.derivation_name exhaust;
     val (thm', thy') = thy
       |> Sign.root_path
       |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)

--- a/src/HOL/Tools/inductive_realizer.ML	Sat May 08 17:10:27 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat May 08 16:53:53 2010 +0200
@@ -408,7 +408,7 @@
       in
         Extraction.add_realizers_i
           (map (fn (((ind, corr), rlz), r) =>
-              mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
+              mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
             realizers @ (case realizers of
              [(((ind, corr), rlz), r)] =>
                [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",

--- a/src/Pure/Proof/extraction.ML	Sat May 08 17:10:27 2010 +0200
+++ b/src/Pure/Proof/extraction.ML	Sat May 08 16:53:53 2010 +0200
@@ -303,7 +303,7 @@
     val rd = Proof_Syntax.read_proof thy' false;
   in fn (thm, (vs, s1, s2)) =>
     let
-      val name = Thm.get_name thm;
+      val name = Thm.derivation_name thm;
       val _ = name <> "" orelse error "add_realizers: unnamed theorem";
       val prop = Pattern.rewrite_term thy'
         (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
@@ -348,7 +348,7 @@
     val {realizes_eqns, typeof_eqns, types, realizers,
       defs, expand, prep} = ExtractionData.get thy;
 
-    val name = Thm.get_name thm;
+    val name = Thm.derivation_name thm;
     val _ = name <> "" orelse error "add_expand_thm: unnamed theorem";
   in
     thy |> ExtractionData.put
@@ -706,7 +706,7 @@
         val thy = Thm.theory_of_thm thm;
         val prop = Thm.prop_of thm;
         val prf = Thm.proof_of thm;
-        val name = Thm.get_name thm;
+        val name = Thm.derivation_name thm;
         val _ = name <> "" orelse error "extraction: unnamed theorem";
         val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
           quote name ^ " has no computational content")

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat May 08 17:10:27 2010 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat May 08 16:53:53 2010 +0200
@@ -244,7 +244,7 @@
 fun elim_defs thy r defs prf =
   let
     val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
-    val defnames = map Thm.get_name defs;
+    val defnames = map Thm.derivation_name defs;
     val f = if not r then I else
       let
         val cnames = map (fst o dest_Const o fst) defs';

--- a/src/Pure/Thy/thm_deps.ML	Sat May 08 17:10:27 2010 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat May 08 16:53:53 2010 +0200
@@ -53,7 +53,7 @@
       else
         let val {concealed, group, ...} = Name_Space.the_entry space name in
           fold_rev (fn th =>
-            (case Thm.get_name th of
+            (case Thm.derivation_name th of
               "" => I
             | a => cons (a, (th, concealed, group)))) ths
         end;

--- a/src/Pure/more_thm.ML	Sat May 08 17:10:27 2010 +0200
+++ b/src/Pure/more_thm.ML	Sat May 08 16:53:53 2010 +0200
@@ -326,7 +326,7 @@
 (* close_derivation *)
 
 fun close_derivation thm =
-  if Thm.get_name thm = "" then Thm.put_name "" thm
+  if Thm.derivation_name thm = "" then Thm.name_derivation "" thm
   else thm;
 
 

--- a/src/Pure/pure_thy.ML	Sat May 08 17:10:27 2010 +0200
+++ b/src/Pure/pure_thy.ML	Sat May 08 16:53:53 2010 +0200
@@ -121,7 +121,7 @@
   | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
 
 fun name_thm pre official name thm = thm
-  |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
+  |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name
   |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
 
 fun name_thms pre official name xs =

--- a/src/Pure/thm.ML	Sat May 08 17:10:27 2010 +0200
+++ b/src/Pure/thm.ML	Sat May 08 16:53:53 2010 +0200
@@ -126,8 +126,8 @@
   val proof_of: thm -> proof
   val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
-  val get_name: thm -> string
-  val put_name: string -> thm -> thm
+  val derivation_name: thm -> string
+  val name_derivation: string -> thm -> thm
   val axiom: theory -> string -> thm
   val axioms_of: theory -> (string * thm) list
   val get_tags: thm -> Properties.T
@@ -585,10 +585,10 @@
 
 (* closed derivations with official name *)
 
-fun get_name thm =
+fun derivation_name thm =
   Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
 
-fun put_name name (thm as Thm (der, args)) =
+fun name_derivation name (thm as Thm (der, args)) =
   let
     val Deriv {promises, body} = der;
     val {thy_ref, hyps, prop, tpairs, ...} = args;