# HG changeset patch # User wenzelm # Date 1737139596 -3600 # Node ID 17831ae5224db756bbbfd3309058440afec544e3 # Parent dc982cbeb54291c6db7e1159b55e991cd4dafaf2 tuned; diff -r dc982cbeb542 -r 17831ae5224d src/HOL/Import/import_data.ML --- a/src/HOL/Import/import_data.ML Fri Jan 17 19:40:56 2025 +0100 +++ b/src/HOL/Import/import_data.ML Fri Jan 17 19:46:36 2025 +0100 @@ -67,13 +67,13 @@ fun add_const_def c th name_opt thy = let val th' = Thm.legacy_freezeT th - val name = + val d = (case name_opt of NONE => dest_Const_name (#1 (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th')))) - | SOME name => name) + | SOME d => d) in thy - |> add_const_map c name + |> add_const_map c d |> Data.map (fn {const_map, ty_map, const_def, ty_def} => {const_map = const_map, ty_map = ty_map, const_def = (Symtab.update (c, th') const_def), ty_def = ty_def})