src/HOL/Tools/Lifting/lifting_bnf.ML

 Setup for Lifting for types that are BNF.
 *)
 
 signature LIFTING_BNF =
 sig
+  val lifting_interpretation: string
 end
 
 structure Lifting_BNF : LIFTING_BNF =
 struct
 
 open BNF_Util
 open BNF_Def
 open Transfer_BNF
+
+val lifting_interpretation = "lifting"
 
 (* Quotient map theorem *)
 
 fun Quotient_tac bnf ctxt i =
   let

         @ relator_distr bnf
     in
       snd (Local_Theory.notes notes lthy)
     end
 
-val _ = Theory.setup (bnf_interpretation
-  (bnf_only_type_ctr (map_local_theory o lifting_bnf_interpretation))
+val _ = Theory.setup (bnf_interpretation lifting_interpretation
+  (bnf_only_type_ctr (BNF_Util.map_local_theory o lifting_bnf_interpretation))
   (bnf_only_type_ctr lifting_bnf_interpretation))
 
 end