diff -r 9ae5c21fc88c -r f21494dc0bf6 src/HOL/Import/import_rews.ML
--- a/src/HOL/Import/import_rews.ML	Sat Mar 03 23:49:54 2012 +0100
+++ b/src/HOL/Import/import_rews.ML	Sat Mar 03 23:54:44 2012 +0100
@@ -158,7 +158,7 @@
 
 fun add_hol4_rewrite (Context.Theory thy, th) =
     let
-        val _ = message "Adding HOL4 rewrite"
+        val _ = message "Adding external rewrite"
         val th1 = th RS @{thm eq_reflection}
                   handle THM _ => th
         val current_rews = HOL4Rewrites.get thy
@@ -359,7 +359,7 @@
 
 fun add_hol4_theorem thyname thmname hth =
   let
-    val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
+    val _ = message ("Adding external theorem " ^ thyname ^ "." ^ thmname)
   in
     HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth))
   end;
@@ -634,6 +634,6 @@
 val hol4_setup =
   initial_maps #>
   Attrib.setup @{binding import_rew}
-    (Scan.succeed (Thm.mixed_attribute add_hol4_rewrite)) "HOL4 rewrite rule"
+    (Scan.succeed (Thm.mixed_attribute add_hol4_rewrite)) "external rewrite rule"
 
 end