# HG changeset patch
# User wenzelm
# Date 1627990817 -7200
# Node ID 228adc5028038f32cf457607484b9eab86ae97a7
# Parent  d0527bb2e59009e6b164c40df74a94f9bda4e32e
proper name space "kind": this is a formal name, not comment;

diff -r d0527bb2e590 -r 228adc502803 src/HOL/Real_Asymp/exp_log_expression.ML
--- a/src/HOL/Real_Asymp/exp_log_expression.ML	Tue Aug 03 13:08:23 2021 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML	Tue Aug 03 13:40:17 2021 +0200
@@ -128,7 +128,7 @@
   fun eq_entry ({name = name1, ...}, {name = name2, ...}) = (name1 = name2)
   val empty = 
     {
-      name_table = Name_Space.empty_table "Exp-Log Custom Function",
+      name_table = Name_Space.empty_table "exp_log_custom_function",
       net = Item_Net.init eq_entry (fn {net_pat, ...} => [net_pat])
     }
   
diff -r d0527bb2e590 -r 228adc502803 src/HOL/Real_Asymp/multiseries_expansion.ML
--- a/src/HOL/Real_Asymp/multiseries_expansion.ML	Tue Aug 03 13:08:23 2021 +0200
+++ b/src/HOL/Real_Asymp/multiseries_expansion.ML	Tue Aug 03 13:40:17 2021 +0200
@@ -135,7 +135,7 @@
 structure Data = Generic_Data
 (
   type T = (Proof.context -> int -> tactic) Name_Space.table;
-  val empty : T = Name_Space.empty_table "sign oracle tactics";
+  val empty : T = Name_Space.empty_table "sign_oracle_tactic";
   val extend = I;
   fun merge (tactics1, tactics2) : T = Name_Space.merge_tables (tactics1, tactics2);
 );