src/HOL/Tools/BNF/bnf_def.ML

   let
     val axioms = axioms_of_bnf bnf;
     val facts = facts_of_bnf bnf;
     val wits = wits_of_bnf bnf;
     val qualify =
-      let val (_, qs, _) = Binding.dest bnf_b;
+      let val qs = Binding.path_of bnf_b;
       in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify0 end;
 
     fun note_if_note_all (noted0, lthy0) =
       let
         val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits);