# 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); );