--- 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])
}
--- 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);
);