--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Dec 02 15:04:38 2019 +0100
@@ -637,7 +637,7 @@
val transfer = exists (can (fn Transfer_Option => ())) opts;
val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
- val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map (#1 o #1) fixes));
+ val spec_name = Binding.conglomerate (map (#1 o #1) fixes);
val mk_notes =
flat oooo @{map 4} (fn js => fn prefix => fn qualify => fn thms =>