src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

       |> the_default Plugin_Name.default_filter;
     val nonexhaustive = exists (can (fn Nonexhaustive_Option => ())) opts;
     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 =>
         let
           val (bs, attrss) = map_split (fst o nth specs) js;