# HG changeset patch
# User aspinall
# Date 1170270384 -3600
# Node ID 6c2373adc7a0ffa367c924f012d984c7d706bcc5
# Parent  69d4b98f4c474934c09eaa92e36d2a5ad7dbc988
Expose hard-wired string which was changed and broke Proof General.

diff -r 69d4b98f4c47 -r 6c2373adc7a0 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Jan 31 16:05:17 2007 +0100
+++ b/src/Pure/pure_thy.ML	Wed Jan 31 20:06:24 2007 +0100
@@ -31,6 +31,7 @@
   val untag_rule: string -> thm -> thm
   val tag: tag -> attribute
   val untag: string -> attribute
+  val unknown_name_hint: string
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
@@ -117,12 +118,14 @@
 
 (* unofficial theorem names *)
 
+val unknown_name_hint = "??.unknown";
+
 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");
+  | _ => unknown_name_hint);
 
 fun put_name_hint name = untag_rule "name" #> tag_rule ("name", [name]);