# HG changeset patch
# User wenzelm
# Date 1167491284 -3600
# Node ID df2e82888a664cd4397ca0aed1c6e6ea48f41859
# Parent  416a5338d2bb0122023357c4f952d4da2d15b75c
added has_name_hint;
name_thm: more careful pre-naming;

diff -r 416a5338d2bb -r df2e82888a66 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Dec 30 16:08:03 2006 +0100
+++ b/src/Pure/pure_thy.ML	Sat Dec 30 16:08:04 2006 +0100
@@ -33,6 +33,7 @@
   val untag_rule: string -> thm -> thm
   val tag: tag -> attribute
   val untag: string -> attribute
+  val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
   val get_kind: thm -> string
@@ -120,13 +121,15 @@
 
 (* unofficial theorem names *)
 
-fun put_name_hint name = untag_rule "name" #> tag_rule ("name", [name]);
+fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) "name";
 
 fun get_name_hint thm =
   (case AList.lookup (op =) (Thm.get_tags thm) "name" of
     SOME (k :: _) => k
   | _ => "??.unknown");
 
+fun put_name_hint name = untag_rule "name" #> tag_rule ("name", [name]);
+
 
 (* theorem kinds *)
 
@@ -338,7 +341,7 @@
 
 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)
-  |> (if get_name_hint thm <> "" andalso pre orelse name = "" then I else put_name_hint name);
+  |> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name);
 
 fun name_thms pre official name xs =
   map (uncurry (name_thm pre official)) (name_multi name xs);