src/HOL/Tools/BNF/bnf_def.ML

     (*|> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers*)
     |> (fn thy => f (morph_bnf (Morphism.transfer_morphism thy) bnf) thy)
     (*|> Sign.restore_naming thy*)
   end;
 
-val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path;
+fun bnf_interpretation f = BNF_Interpretation.interpretation (with_repaired_path f);
 
 fun register_bnf key bnf =
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)))
   #> Local_Theory.background_theory (BNF_Interpretation.data bnf);